;;;===========================================================================
;;;
;;; SES 3 Theorem
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 27/05/10 || End date: 28/05/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "cone2-equivalence-theorem-structure")


(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring-R *) => *)
 ;; Addition operation ring
 ((addition-ring-R * *)=> *)
 ;; Product operation ring
 ((product-ring-R * *) => *)
 ;; Inverse ring
 ((inverse-R *) => *)
 ;; Zero element ring
 ((zero-element-R ) => *)
 ;; Unit element ring
 ((unit-R )=> *)

 ;;--------------------------------------------------
 ;; We want to find the homotopye equivalence C_C <<= D_C =>> H_C
 ;;--------------------------------------------------


;;--------------------------------------------------
 ;; First homotopy equivalence CA <<= DA =>> HA
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; CA Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-CA * *) => *)
 ;; Group Operation 
 ((group-operation-CA * * *) => *)
 ;; Zero element
 ((zero-CA *) => *)
 ;; External multiplication
 ((external-CA * * *) => *)
 ;; Inverse element
 ((inverse-CA * *) => *)

 ;;--------------------------------------------------
 ;; The CA differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-CA * *) => *)

 ;;--------------------------------------------------
 ;; DA Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-DA * *) => *)
 ;; Group Operation 
 ((group-operation-DA * * *) => *)
 ;; Zero element
 ((zero-DA *) => *)
 ;; External multiplication
 ((external-DA * * *) => *)
 ;; Inverse element
 ((inverse-DA * *) => *)

 ;;--------------------------------------------------
 ;; The DA differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-DA * *) => *)

  ;;--------------------------------------------------
 ;; HA Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-HA * *) => *)
 ;; Group Operation 
 ((group-operation-HA * * *) => *)
 ;; Zero element
 ((zero-HA *) => *)
 ;; External multiplication
 ((external-HA * * *) => *)
 ;; Inverse element
 ((inverse-HA * *) => *)

 ;;--------------------------------------------------
 ;; The HA differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-HA * *) => *)

 ;;--------------------------------------------------
 ;; Second homotopy equivalence CB <<= DB =>> HB
 ;;--------------------------------------------------


 ;;--------------------------------------------------
 ;; CB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-CB * *) => *)
 ;; Group Operation 
 ((group-operation-CB * * *) => *)
 ;; Zero element
 ((zero-CB *) => *)
 ;; External multiplication
 ((external-CB * * *) => *)
 ;; Inverse element
 ((inverse-CB * *) => *)

 ;;--------------------------------------------------
 ;; The CB differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-CB * *) => *)

 ;;--------------------------------------------------
 ;; DB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-DB * *) => *)
 ;; Group Operation 
 ((group-operation-DB * * *) => *)
 ;; Zero element
 ((zero-DB *) => *)
 ;; External multiplication
 ((external-DB * * *) => *)
 ;; Inverse element
 ((inverse-DB * *) => *)

 ;;--------------------------------------------------
 ;; The DB differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-DB * *) => *)

  ;;--------------------------------------------------
 ;; HB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-HB * *) => *)
 ;; Group Operation 
 ((group-operation-HB * * *) => *)
 ;; Zero element
 ((zero-HB *) => *)
 ;; External multiplication
 ((external-HB * * *) => *)
 ;; Inverse element
 ((inverse-HB * *) => *)

 ;;--------------------------------------------------
 ;; The HB differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-HB * *) => *)

 
 
 ;;--------------------------------------------------
 ;; C_C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C_C * *) => *)
 ;; Group Operation 
 ((group-operation-C_C * * *) => *)
 ;; Zero element
 ((zero-C_C *) => *)
 ;; External multiplication
 ((external-C_C * * *) => *)
 ;; Inverse element
 ((inverse-C_C * *) => *)

 ;;--------------------------------------------------
 ;; The C_C differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-C_C * *) => *)


 
 ;;--------------------------------------------------
 ;; Morphisms of the first homotopy equivalence
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; The lfA morphism
 ;;--------------------------------------------------

 ;; The function
 ((lfA * *) => *)

 ;;--------------------------------------------------
 ;; The lgA CA morphism
 ;;--------------------------------------------------

 ;; The function
 ((lgA * *) => *)


 ;;--------------------------------------------------
 ;; The lhA CA morphism
 ;;--------------------------------------------------

 ;; The function
 ((lhA * *) => *)

 ;;--------------------------------------------------
 ;; The rfA morphism
 ;;--------------------------------------------------

 ;; The function
 ((rfA * *) => *)

 ;;--------------------------------------------------
 ;; The rgA CA morphism
 ;;--------------------------------------------------

 ;; The function
 ((rgA * *) => *)


 ;;--------------------------------------------------
 ;; The rhA CA morphism
 ;;--------------------------------------------------

 ;; The function
 ((rhA * *) => *)


 ;;--------------------------------------------------
 ;; Morphisms of the second homotopy equivalence
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; The lfB morphism
 ;;--------------------------------------------------

 ;; The function
 ((lfB * *) => *)

 ;;--------------------------------------------------
 ;; The lgB CB morphism
 ;;--------------------------------------------------

 ;; The function
 ((lgB * *) => *)


 ;;--------------------------------------------------
 ;; The lhB CB morphism
 ;;--------------------------------------------------

 ;; The function
 ((lhB * *) => *)

 ;;--------------------------------------------------
 ;; The rfB morphism
 ;;--------------------------------------------------

 ;; The function
 ((rfB * *) => *)

 ;;--------------------------------------------------
 ;; The rgB CB morphism
 ;;--------------------------------------------------

 ;; The function
 ((rgB * *) => *)


 ;;--------------------------------------------------
 ;; The rhB CB morphism
 ;;--------------------------------------------------

 ;; The function
 ((rhB * *) => *)

 ;;--------------------------------------------------
 ;; sigma : A -> B
 ;;--------------------------------------------------

 ((sigma * *) => *)

 ;;--------------------------------------------------
 ;; j : B -> A
 ;;--------------------------------------------------

 ((j * *) => *)
 
 ;;--------------------------------------------------
 ;; rho : B -> C
 ;;--------------------------------------------------

 ((rho * *) => *)

 ;;--------------------------------------------------
 ;; i : C -> B
 ;;--------------------------------------------------

 ((i * *) => *)
 

 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring-R (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring-R (a b)
	  (+ a b)))

 ;; Product operation ring
 (local (defun product-ring-R (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse-R (a)
	  (- a)))

 ;; Zero element ring
 (local (defun zero-element-R nil
	  0))

 ;; Unit element ring
 (local (defun unit-R nil
	  1))

 ;;--------------------------------------------------
 ;; CA Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-CA (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-CA (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-CA (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-CA (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-CA (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The CA differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-CA (n a)
	  (declare (ignore n a))
	  0))



 ;;--------------------------------------------------
 ;; DA Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-DA (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-DA (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-DA (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-DA (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-DA (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The DA differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-DA (n a)
	  (declare (ignore n a))
	  0))


  ;;--------------------------------------------------
 ;; HC Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-HA (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-HA (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-HA (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-HA (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-HA (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The HA differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-HA (n a)
	  (declare (ignore n a))
	  0))



 ;;--------------------------------------------------
 ;; CB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-CB (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-CB (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-CB (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-CB (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-CB (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The CB differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-CB (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; DB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-DB (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-DB (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-DB (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-DB (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-DB (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The DB differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-DB (n a)
	  (declare (ignore n a))
	  0))


  ;;--------------------------------------------------
 ;; HB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-HB (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-HB (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-HB (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-HB (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-HB (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The HB differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-HB (n a)
	  (declare (ignore n a))
	  0))
 


 ;;--------------------------------------------------
 ;; C_C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C_C (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C_C (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C_C (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C_C (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-C_C (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The C_C differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-C_C (n a)
	  (declare (ignore n a))
	  0))



 ;;--------------------------------------------------
 ;; The lfA morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lfA (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lgA morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lgA (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lhA morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lhA (n a)
	  (declare (ignore n a))
	  0))


;;--------------------------------------------------
 ;; The rfA morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rfA (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The rgA morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rgA (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The rhA morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rhA (n a)
	  (declare (ignore n a))
	  0))


 

 ;;--------------------------------------------------
 ;; The lfB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lfB (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lgB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lgB (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lhB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lhB (n a)
	  (declare (ignore n a))
	  0))


;;--------------------------------------------------
 ;; The rfB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rfB (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The rgB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rgB (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The rhB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rhB (n a)
	  (declare (ignore n a))
	  0))






 ;;--------------------------------------------------
 ;; sigma : A -> B
 ;;--------------------------------------------------

 (local (defun sigma (n a)
	(declare (ignore n a))
	  0
	))

 ;;--------------------------------------------------
 ;; j : B -> A
 ;;--------------------------------------------------

 (local (defun j (n a)
	(declare (ignore n a))
	  0
	))
 
 
 ;;--------------------------------------------------
 ;; rho : B -> C
 ;;--------------------------------------------------

(local (defun rho (n a)
	(declare (ignore n a))
	  0
	))
 

 ;;--------------------------------------------------
 ;; i : C -> B
 ;;--------------------------------------------------

(local (defun i (n a)
	(declare (ignore n a))
	  0
	))
 

 

  ;;************************************************** 
  ;; Properties
  ;;**************************************************

(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-DA 'group-operation-DA 'zero-DA 'external-DA 'inverse-DA 'd-DA )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
    'inv-CA 'group-operation-CA 'zero-CA 'external-CA 'inverse-CA 'd-CA )
  'lfA  'lgA  'lhA
  )
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-DA 'group-operation-DA 'zero-DA 'external-DA 'inverse-DA 'd-DA )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
    'inv-HA 'group-operation-HA 'zero-HA 'external-HA 'inverse-HA 'd-HA )
  'rfA  'rgA  'rhA
  ))
 'homotopy-equivalence-A
   )


(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-DB 'group-operation-DB 'zero-DB 'external-DB 'inverse-DB 'd-DB )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
    'inv-CB 'group-operation-CB 'zero-CB 'external-CB 'inverse-CB 'd-CB )
  'lfB  'lgB  'lhB
  )
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-DB 'group-operation-DB 'zero-DB 'external-DB 'inverse-DB 'd-DB )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
    'inv-HB 'group-operation-HB 'zero-HB 'external-HB 'inverse-HB 'd-HB )
  'rfB  'rgB  'rhB
  ))
 'homotopy-equivalence-B
   )


(check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring-R :addition-ring 'addition-ring-R :zero-element 'zero-element-R
		    :inverse 'inverse-R :product-ring 'product-ring-R :unit 'unit-R
		    :inv-cc 'inv-C_C :group-operation-cc 'group-operation-C_C :zero-cc 'zero-C_C :external-cc 'external-C_C
		    :inverse-cc 'inverse-C_C :d-cc 'd-C_C)
 'CC)

 
(check-chain-complex-morphism-degree-0-p
(chain-complex-morphism-degree-0 
 (chain-complex 'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 'inv-CB 'group-operation-CB 'zero-CB 'external-CB 'inverse-CB 'd-CB )
 (chain-complex 'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 'inv-CA 'group-operation-CA 'zero-CA 'external-CA 'inverse-CA 'd-CA )
 'j) 'j)


(check-chain-complex-morphism-degree-0-p
(chain-complex-morphism-degree-0 
 (chain-complex 'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 'inv-C_C 'group-operation-C_C 'zero-C_C 'external-C_C 'inverse-C_C 'd-C_C )
 (chain-complex 'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 'inv-CB 'group-operation-CB 'zero-CB 'external-CB 'inverse-CB 'd-CB )
 'i) 'i)


(check-morphism-degree-0-p
(morphism-degree-0 'inv-CA 'inv-CB 'sigma  'group-operation-CA 'group-operation-CB
		   'external-CA 'external-CB 'inv-ring-R
		   'zero-CA 'zero-CB 'inverse-CA 'inverse-CB )
'sigma
)

(check-morphism-degree-0-p
(morphism-degree-0  'inv-CB 'inv-C_C 'rho  'group-operation-CB 'group-operation-C_C
		    'external-CB 'external-C_C 'inv-ring-R
		    'zero-CB 'zero-C_C 'inverse-CB 'inverse-C_C )
'rho
)


(defthm rho-i
  (implies (and (inv-C_C n a)
		(integerp n))
	   (equal (rho n (i n a))
		  a)))

(defthm i-rho+sigma-j
  (implies (and (inv-CB n a)
		(integerp n))
	   (equal (group-operation-CB n (i n (rho n a))
				      (sigma n (j n a)))
		  a)))

(defthm j-sigma
  (implies (and (inv-CA n a)
		(integerp n))
	   (equal (j n (sigma n a))
		  a)))


(defthm rho-sigma
  (implies (and (inv-CA n a)
		(integerp n))
	   (equal (rho n (sigma n a))
		  (zero-C_C n))))


(defthm j-i
  (implies (and (inv-C_C n c)
		(integerp n))
	   (equal (j n (i n c))
		  (zero-CA n))))

(defthm i=inverse-i
  (implies (and (inv-C_C n c)
		(integerp n))
	   (equal (inverse-cb n (i n c))
		  (i n c))))
		
)

;;;**************************************************
;;;
;;; Definition of the Equivalence of the Cone(j)
;;;
;;;**************************************************



(defthm prop1 (IMPLIES (AND (INV-CA N A)
              (INV-CA N B)
              (INV-CA N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-CA N (GROUP-OPERATION-CA N A B) C)
                (GROUP-OPERATION-CA N A (GROUP-OPERATION-CA N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-A-is-an-homotopy-equivalence|)))))


(defthm prop2
  (IMPLIES (AND (INV-CA N A) (INTEGERP N))
         (INV-CA (+ N -1) (D-CA N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-A-is-an-homotopy-equivalence|)))))




(defthm prop3 (IMPLIES (AND (INV-CB N A)
              (INV-CB N B)
              (INV-CB N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-CB N (GROUP-OPERATION-CB N A B) C)
                (GROUP-OPERATION-CB N A (GROUP-OPERATION-CB N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))

(defthm prop_4 (IMPLIES (AND (INV-DB N A)
              (INV-DB N B)
              (INV-DB N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-DB N (GROUP-OPERATION-DB N A B) C)
                (GROUP-OPERATION-DB N A (GROUP-OPERATION-DB N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))

(defthm prop5 (IMPLIES (AND (INV-HB N A)
              (INV-HB N B)
              (INV-HB N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-HB N (GROUP-OPERATION-HB N A B) C)
                (GROUP-OPERATION-HB N A (GROUP-OPERATION-HB N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))


(defthm prop6 (IMPLIES (AND (INV-DA N A)
              (INV-DA N B)
              (INV-DA N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-DA N (GROUP-OPERATION-DA N A B) C)
                (GROUP-OPERATION-DA N A (GROUP-OPERATION-DA N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-A-is-an-homotopy-equivalence|)))))

(defthm prop7 (IMPLIES (AND (INV-HA N A)
              (INV-HA N B)
              (INV-HA N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-HA N (GROUP-OPERATION-HA N A B) C)
                (GROUP-OPERATION-HA N A (GROUP-OPERATION-HA N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-A-is-an-homotopy-equivalence|)))))

(defthm prop8
  (IMPLIES (AND (INV-CB N A) (INTEGERP N))
         (INV-CB (+ N -1) (D-CB N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))


(defthm prop9
  (IMPLIES (AND (INV-DB N A) (INTEGERP N))
         (INV-DB (+ N -1) (D-DB N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))



(defthm prop10
  (IMPLIES (AND (INV-HB N A) (INTEGERP N))
         (INV-HB (+ N -1) (D-HB N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))



(defthm prop11
  (IMPLIES (AND (INV-DA N A) (INTEGERP N))
         (INV-DA (+ N -1) (D-DA N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-A-is-an-homotopy-equivalence|)))))





(defthm prop12
  (IMPLIES (AND (INV-HA N A) (INTEGERP N))
         (INV-HA (+ N -1) (D-HA N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-A-is-an-homotopy-equivalence|)))))



(defthm prop13
  (IMPLIES (AND (INV-DA N A) (INTEGERP N))
	   (INV-DA (+ N 1) (LHA N A)))
  :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-A-is-an-homotopy-equivalence|)))))



(defthm prop14
  (IMPLIES (AND (INV-DA N A) (INTEGERP N))
         (INV-DA (+ N 1) (RHA N A)))
  :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-A-is-an-homotopy-equivalence|)))))




(defthm prop15
  (IMPLIES (AND (INV-DB N A) (INTEGERP N))
         (INV-DB (+ n 1) (LHB N A)))
  :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))




(defthm prop16
  (IMPLIES (AND (INV-DB N A) (INTEGERP N))
         (INV-DB (+ n 1) (RHB N A)))
  :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))


(definstance-*CONE-REDUCTION-THEOREM-v2*
  ((inv-ring-Z inv-ring-R)
    (addition-ring-Z addition-ring-R)
    (product-ring-Z product-ring-R)
    (inverse-Z inverse-R)
    (zero-element-Z zero-element-R)
    (unit-Z unit-R)
    (inv-C1 inv-CA)
    (group-operation-C1 group-operation-CA)
    (zero-C1 zero-CA)
    (external-C1 external-CA)
    (inverse-C1 inverse-CA)
    (d-C1 d-CA)
    (inv-D1 inv-DA)
    (group-operation-D1 group-operation-DA)
    (zero-D1 zero-DA)
    (external-D1 external-DA)
    (inverse-D1 inverse-DA)
    (d-D1 d-DA)
    (inv-H1 inv-HA)
    (group-operation-H1 group-operation-HA)
    (zero-H1 zero-HA)
    (external-H1 external-HA)
    (inverse-H1 inverse-HA)
    (d-H1 d-HA)
    (inv-C2 inv-CB)
    (group-operation-C2 group-operation-CB)
    (zero-C2 zero-CB)
    (external-C2 external-CB)
    (inverse-C2 inverse-CB)
    (d-C2 d-CB)
    (inv-D2 inv-DB)
    (group-operation-D2 group-operation-DB)
    (zero-D2 zero-DB)
    (external-D2 external-DB)
    (inverse-D2 inverse-DB)
    (d-D2 d-DB)
    (inv-H2 inv-HB)
    (group-operation-H2 group-operation-HB)
    (zero-H2 zero-HB)
    (external-H2 external-HB)
    (inverse-H2 inverse-HB)
    (d-H2 d-HB)
    (lf1 lfA)
    (lg1 lgA)
    (lh1 lhA)
    (rf1 rfA)
    (rg1 rgA)
    (rh1 rhA)
    (lf2 lfB)
    (lg2 lgB)
    (lh2 lhB)
    (rf2 rfB)
    (rg2 rgB)
    (rh2 rhB)
    (phi-c2-c1 j))
  "-cone-SES3")




;;;**************************************************
;;;
;;; Definition of the functions of Reduction Cone(j) =>> C_C
;;;
;;;**************************************************



(defun f-cone-C (n a)
  (group-operation-C_C n (rho n (cadr a))
		       (rho n (d-CB (1+ n) (sigma (1+ n) (car a))))))
 

(defun g-cone-C (n a)
  (list (zero-CA (1+ n))
	(i n a))
  )



(defun h-cone-cone (n a)
  (list (zero-CA (1+ (1+ n)))
	(sigma (1+ n) (car a))))



;;;**************************************************
;;; Auxiliar lemmas
;;;**************************************************



(defthm group-operation-cb-commutativity
  (IMPLIES (AND (INV-CB N A)
		(INV-CB N B)
		(integerp n))
         (EQUAL (GROUP-OPERATION-CB N A B)
                (GROUP-OPERATION-CB N B A)))
  :rule-classes nil)


(defthm lemma1
  (IMPLIES (AND (INV-CB N a)
		(INV-CB N b )
		(INV-CB N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-CB N a (GROUP-OPERATION-CB N b c))
                (GROUP-OPERATION-CB N c (GROUP-OPERATION-CB N a b)))) 
:hints (("Goal" :use ((:instance prop3)
		      (:instance  group-operation-cb-commutativity
				  (a c)
				  (b (GROUP-OPERATION-CB N a b)))))))


(defthm lemma1-bis
  (IMPLIES (AND (INV-CB N a)
		(INV-CB N b )
		(INV-CB N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-CB N a (GROUP-OPERATION-CB N b c))
                (GROUP-OPERATION-CB N b (GROUP-OPERATION-CB N a c)))) 
:hints (("Goal" :use ((:instance prop3)
		      (:instance  group-operation-cb-commutativity
				  (a b)
				  (b (GROUP-OPERATION-CB N a c)))))))

(defthm group-operation-cc-commutativity
  (IMPLIES (AND (INV-C_c N A)
		(INV-C_C N B)
		(integerp n))
         (EQUAL (GROUP-OPERATION-C_c N A B)
                (GROUP-OPERATION-C_c N B A)))
  :rule-classes nil)



(defthm prop3_CC (IMPLIES (AND (INV-C_C N A)
              (INV-C_C N B)
              (INV-C_C N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C_C N (GROUP-OPERATION-C_C N A B) C)
                (GROUP-OPERATION-C_C N A (GROUP-OPERATION-C_C N B C)))) 
:hints (("Goal" :use ((:instance |CC-is-a-chain-complex|)))))


(defthm lemma2
  (IMPLIES (AND (INV-C_C N a)
		(INV-C_C N b )
		(INV-C_C N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-C_C N a (GROUP-OPERATION-C_C N b c))
                (GROUP-OPERATION-C_C N c (GROUP-OPERATION-C_C N a b)))) 
:hints (("Goal" :use ((:instance prop3_CC)
		      (:instance  group-operation-cc-commutativity
				  (a c)
				  (b (GROUP-OPERATION-C_C N a b)))))))


(defthm lemma2-bis
  (IMPLIES (AND (INV-C_C N a)
		(INV-C_C N b )
		(INV-C_C N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-C_C N a (GROUP-OPERATION-C_C N b c))
                (GROUP-OPERATION-C_C N b (GROUP-OPERATION-C_C N a c)))) 
:hints (("Goal" :use ((:instance prop3_CC)
		      (:instance  group-operation-cc-commutativity
				  (a b)
				  (b (GROUP-OPERATION-C_C N a c)))))))

(defthm group-operation-ca-commutativity
  (IMPLIES (AND (INV-Ca N A)
		(INV-Ca N B)
		(integerp n))
         (EQUAL (GROUP-OPERATION-Ca N A B)
                (GROUP-OPERATION-Ca N B A))))

(in-theory (disable group-operation-ca-commutativity))


(defthm prop17 (IMPLIES (AND (INV-Ca N A)
              (INV-Ca N B)
              (INV-Ca N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-CA N (GROUP-OPERATION-CA N A B) C)
                (GROUP-OPERATION-CA N A (GROUP-OPERATION-CA N B C)))) 
)

(defthm lemma3
  (IMPLIES (AND (INV-Ca N a)
		(INV-Ca N b)
		(INV-Ca N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-Ca N a (GROUP-OPERATION-Ca N b c))
		(GROUP-OPERATION-Ca N c (GROUP-OPERATION-Ca N a b))
                )) 
:hints (("Goal" :use (
		      (:instance  group-operation-ca-commutativity
				  (a c)
				  (b (GROUP-OPERATION-Ca N a b)))))))


(defthm lemma3-bis
  (IMPLIES (AND (INV-Ca N a)
		(INV-Ca N b)
		(INV-Ca N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-Ca N a (GROUP-OPERATION-Ca N b c))
		(GROUP-OPERATION-Ca N b (GROUP-OPERATION-Ca N a c))
                )) 
:hints (("Goal" :use (
		      (:instance  group-operation-ca-commutativity
				  (a b)
				  (b (GROUP-OPERATION-Ca N a c)))))))

(defthm lemma4
  (implies (and (inv-ca n a)
		(integerp n))
	   (inv-ca (+ n -1) (d-ca n a))))


(defthm inv-ca+1+n-1
  (implies (integerp n)
	   (equal (inv-ca (+ 1 n -1) a)
		  (inv-ca n a)))
  :hints (("Goal" :use (:instance |+1+N-1=N|))))

(defthm inv-n-d-ca+1+n-help
  (implies (and (inv-ca n a)
		(integerp n))
	   (inv-ca (+ n -1) (d-ca n a))))

(defthm inv-n-d-ca+1+n
  (implies (and (inv-ca (+ 1 n) a)
		(integerp n))
	   (inv-ca n (d-ca (+ 1 n) a)))
  :hints (("Goal" :use ((:instance inv-n-d-ca+1+n-help (n (+ 1 n)))
			(:instance |+1+N-1=N|)))))


(defthm inverse-cb+n-1
  (implies (integerp n)
	   (equal (inverse-cb (+ -1 N) a)
		  (inverse-cb (+ N -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))


(defthm group-operation-ca+1+n-1
  (implies (integerp n)
	   (equal (group-operation-ca (+ 1 N -1) a b)
		  (group-operation-ca n a b)))
  :hints (("Goal" :use (:instance |+1+N-1=N|))))


(defthm external-ca+1+n-1
  (implies (integerp n)
	   (equal (external-ca (+ 1 N -1) a b)
		  (external-ca n a b)))
  :hints (("Goal" :use (:instance |+1+N-1=N|))))


(defthm zero-ca+1+n-1
  (implies (integerp n)
	   (equal (zero-ca (+ 1 N -1))
		  (zero-ca n)))
  :hints (("Goal" :use (:instance |+1+N-1=N|))))

(defthm inverse-ca+1+n-1
  (implies (integerp n)
	   (equal (inverse-ca (+ 1 N -1) a )
		  (inverse-ca n a )))
  :hints (("Goal" :use (:instance |+1+N-1=N|))))


(defthm j-cb+n-1
  (implies (integerp n)
	   (equal (j (+ -1 N) a)
		  (j (+ N -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))

(defthm d-ca+1-1+n
  (implies (integerp n)
	   (equal (d-ca (+ 1 -1 N) a)
		  (d-ca n a )))
  :hints (("Goal" :use (:instance |+1-1+N=N|))))


(defthm zero-ca+1-1-1+n
  (implies (integerp n)
	   (equal (zero-ca (+ 1 -1 -1 N))
		  (zero-ca (+ n -1) )))
  :hints (("Goal" :use 
	   ((:instance |+1-1-1+N=N-1|)
	     (:instance |+N-1=-1+N|)))))

(defthm group-operation-ca+n-1
  (implies (integerp n)
	   (equal (group-operation-ca (+ -1 N) a b)
		  (group-operation-ca (+ N -1) a b)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))

(defthm d-ca-d-ca+1+n-help
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (d-ca (1- n) (d-ca n a))
		  (zero-ca (1- (1- n))))))


(defthm d-ca-d-ca+1+n-help-2
  (implies (and (inv-ca (+ 1 N) a)
		(integerp n))
	   (equal (d-ca (1- (+ 1 N)) (d-ca (+ 1 N) a))
		  (zero-ca (1- (1- (+ 1 N)))))))

(defthm d-ca-d-ca+1+n
  (implies (and (inv-ca (+ 1 N) a)
		(integerp n))
	   (equal (d-ca n (d-ca (+ 1 N) a))
		  (zero-ca (+ n -1))))
  :hints (("Goal" :use ((:instance |-1-1+1+N=-1+N|)
			(:instance |-1+1+N=N|)
			(:instance |+N-1=-1+N|)
			(:instance d-ca-d-ca+1+n-help-2)))))


(defthm d-ca-d-ca+n+1
  (implies (and (inv-ca (+ 1 N) a)
		(integerp n))
	   (equal (d-ca n (d-ca (+ N 1) a))
		  (zero-ca (+ n -1))))
  :hints (("Goal" :use ((:instance  d-ca-d-ca+1+n)
			(:instance |+1+N=N+1|)))))


(defthm d-cb+n-1
  (implies (integerp n)
	   (equal (d-cb (+ -1 N) a)
		  (d-cb (+ N -1) a)))
  :hints (("Goal" :use (:instance |+N-1=-1+N|))))

(defthm inverse-cb-inverse-cb+n-2
  (implies (and (inv-cb (+ n -2) a)
		(integerp n))
	   (equal (INVERSE-CB (+ N -2) (INVERSE-CB (+ N -2) a))
		  a)))
			

(defthm inv-n-d-cb+1+n-help
  (implies (and (inv-cb n a)
		(integerp n))
	   (inv-cb (+ n -1) (d-cb n a))))


(defthm inv-n-d-cb+1+n
  (implies (and (inv-cb (+ n -1) a)
		(integerp n))
	   (inv-cb (+ n -2) (d-cb (+ n -1) a)))
  :hints (("Goal" :use ((:instance inv-n-d-cb+1+n-help (n (+ n -1)))
			))))

(DEFTHM |-1+N=N-1| (EQUAL (+ -1 N) (+ N -1))
  :RULE-CLASSES NIL)

(defthm d-cb-d-cb+1+n-help
  (implies (and (inv-cb n a)
		(integerp n))
	   (equal (d-cb (+ n -1) (d-cb n a))
		  (zero-cb (1- (1- n)))))
    :hints (("Goal" :in-theory (disable D-CB+N-1)
	     :use (:instance |-1+N=N-1|))))

(defthm d-cb+1+n
  (implies (integerp n)
	   (equal (d-cb (+ 1 N) a)
		  (d-cb (+ N 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm sigma+1+n
  (implies (integerp n)
	   (equal (sigma (+ 1 N) a)
		  (sigma (+ N 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm inv-n-d-cb+n+1
  (implies (and (inv-cb (+ n 1) a)
		(integerp n))
	   (inv-cb n (d-cb (+ n 1) a)))
  :hints (("Goal" :use ((:instance inv-n-d-cb+1+n-help (n (+ n 1)))
			(:instance |+N+0=N|)))))


(defthm inv-rho
  (implies (and (inv-cb n a)
		(integerp n))
	   (inv-c_c n (rho n a))))

(defthm inv-sigma+1+n
  (implies (and (inv-ca (+ 1 n) a)
		(integerp n))
	   (inv-cb (+ n 1) (sigma (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm inv-group-operation-c_c
  (implies (and (inv-c_c n a)
		(inv-c_c n b)
		(integerp n))
	   (inv-c_c n (group-operation-c_c n a b))))

(defthm group-operation-cb+1+n-1
  (implies (integerp n)
	   (equal (group-operation-cb (+ 1 N -1) a b)
		  (group-operation-cb n a b)))
   :hints (("Goal" :use (:instance |+1+N-1=N|))))

(defthm external-cb+1+n-1
  (implies (integerp n)
	   (equal (external-cb (+ 1 N -1) a b)
		  (external-cb n a b)))
   :hints (("Goal" :use (:instance |+1+N-1=N|))))


(defthm zero-cb+1+n-1
  (implies (integerp n)
	   (equal (zero-cb (+ 1 N -1))
		  (zero-cb n)))
   :hints (("Goal" :use (:instance |+1+N-1=N|))))


(defthm inverse-cb+1+n-1
  (implies (integerp n)
	   (equal (inverse-cb (+ 1 N -1) a )
		  (inverse-cb n a )))
   :hints (("Goal" :use (:instance |+1+N-1=N|))))

(defthm sigma-1+n+1
  (implies (integerp n)
	   (equal (sigma (+ -1 N 1) a)
		  (sigma n a)))
   :hints (("Goal" :use (:instance |-1+N+1=N|))))

(defthm d-cb+n+0
  (implies (integerp n)
	   (equal (d-cb (+ n 0) a)
		  (d-cb n a)))
  :hints (("Goal" :use (:instance |+N+0=N|))))


(defthm rho-1+n
  (implies (integerp n)
	   (equal (rho (+ -1 N) a)
		  (rho (+ N -1) a)))
  :hints (("Goal" :use (:instance |-1+N=N-1|))))

(defthm group-operation-cc-1+n
  (implies (integerp n)
	   (equal (group-operation-c_c (+ -1 N) a b)
		  (group-operation-c_c (+ N -1) a b)))
  :hints (("Goal" :use (:instance |-1+N=N-1|))))

(defthm d-ca+n+1
  (implies (integerp n)
	   (equal (d-ca (+ 1 n) a)
		  (d-ca (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))

(defthm inv-ca+1+n+1
  (implies (integerp n)
	   (equal (zero-ca (+ 1 1 n))
		  (zero-ca (+ 1 N 1))))
   :hints (("Goal" :use (:instance |+1+N=N+1|))))

(defthm group-operation-ca+1+n
  (implies (integerp n)
	   (equal (group-operation-ca (+ 1 N) a b)
		  (group-operation-ca (+ N 1) a b)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm d-ca-group-operation
  (implies (and (inv-ca (+ 1 N) a)
		(inv-ca (+ 1 N) b)
		(integerp n))
	   (equal (group-operation-ca n (d-ca (+ N 1) a) (d-ca (+ N 1) b))
		  (d-ca (+ N 1) (group-operation-ca (+ N 1) a b))))
  :hints (("Goal" :in-theory (disable D-CA+N+1 GROUP-OPERATION-CA+1+N)
	   :use ((:instance |+1+N=N+1|)
		 (:instance |+N+0=N|)))))

(defthm d-ca-external
  (implies (and (inv-ca (+ 1 N) a)
		(inv-ring-r r)
		(integerp n))
	   (equal (external-ca n r (d-ca (+ N 1) a))
		  (d-ca (+ N 1) (external-ca (+ 1 n) r a))))
  :hints (("Goal" :in-theory (disable D-CA+N+1 GROUP-OPERATION-CA+1+N)
	   :use ((:instance |+1+N=N+1|)
		 (:instance |+N+0=N|)))))

(defthm zero-ca+1+n
  (implies (integerp n)
	   (equal (ZERO-CA (+ 1 N))
		  (ZERO-CA (+ N 1))))
  :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)))))

(defthm zero-ca+n+0
  (implies (integerp n)
	   (equal (ZERO-CA (+ N 0))
		  (ZERO-CA n)))
  :hints (("Goal" 
	   :use ((:instance |+N+0=N|)))))


(defthm inverse-ca+1+n
  (implies (integerp n)
	   (equal (inverse-CA (+ 1 N) a)
		  (inverse-CA (+ N 1) a)))
  :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)))))


(defthm d-ca-inverse
  (implies (and (inv-ca (+ 1 N) a)
		(integerp n))
	   (equal (inverse-ca n (d-ca (+ N 1) a))
		  (d-ca (+ N 1) (inverse-ca (+ n 1) a))))
  :hints (("Goal" :in-theory (disable D-CA+N+1 GROUP-OPERATION-CA+1+N)
	   :use ((:instance |+1+N=N+1|)
		 (:instance |+N+0=N|)))))


(defthm d-ca-1+n+1
  (implies (integerp n)
	   (equal (d-ca (+ -1 N 1) a)
		  (d-ca n a)))
  :hints (("Goal" :use (:instance |-1+N+1=N|))))


(DEFTHM |-1-1+N=N-2|
  (IMPLIES (INTEGERP N)
	   (EQUAL (+ -1 -1 N) (+ N -2)))
  :RULE-CLASSES NIL)

(defthm zero-1-1+n
  (implies (integerp n)
	   (equal (ZERO-CB (+ -1 -1 N))
		  (ZERO-CB (+ N -2))))
  :hints (("Goal" :use (:instance |-1-1+N=N-2|))))


(defthm inv-ca+1+n
  (implies (integerp n)
	   (equal (inv-ca (+ 1 N) a)
		  (inv-ca (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))



(defthm external-ca+1+n
  (implies (integerp n)
	   (equal (external-ca (+ 1 N) a b)
		  (external-ca (+ n 1) a b)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm group-operation-ca-group-operation-ca
  (implies (and (inv-ca n a)
		(inv-ca n b)
		(inv-ca n c)
		(inv-ca n d)
		(integerp n))
	   (equal (group-operation-ca n (group-operation-ca (+ n 0) a b) (group-operation-ca n c d))
		  (group-operation-ca (+ n 0) (group-operation-ca n c a) (group-operation-ca n d b))
		  ))
  :hints (("Goal" :use (:instance |+N+0=N|))))



(defthm external-ca+n+0
  (implies (and (inv-ca n a)
		(inv-ca n b)
		(inv-ring-r r)
		(integerp n))
	   (equal (group-operation-ca n (external-ca (+ n 0) r a) (external-ca n r b))
		  (external-ca (+ n 0) r  (group-operation-ca n b a))
		  ))
  :hints (("Goal" :use (:instance |+N+0=N|))))


(defthm inverse-ca+n+0
  (implies (and (inv-ca n a)
		(inv-ca n b)
		(integerp n))
	   (equal (group-operation-ca n (inverse-ca (+ n 0) a) (inverse-ca n b))
		  (inverse-ca (+ n 0)  (group-operation-ca n b a))
		  ))
  :hints (("Goal" :use (:instance |+N+0=N|))))


(defthm -1-1+n-1=n-1
  (implies (integerp n)
	   (equal (+ -1 -1 N 1)
		  (+ N -1)))
  :rule-classes nil)

(defthm zero-ca+n-1
  (implies (integerp n)
	   (equal (ZERO-CA (+ -1 -1 N 1))
		  (ZERO-CA (+ N -1))))
  :hints (("Goal" :use (:instance |-1-1+N-1=N-1|))))

(defthm group-operation-cb+n+0
  (implies (integerp n)
	   (equal (group-operation-cb (+ N 0) a b)
		  (group-operation-cb n a b)))
:hints (("Goal" :use (:instance |+N+0=N|))))


(defthm external-cb+n+0
  (implies (integerp n)
	   (equal (external-cb (+ N 0) a b)
		  (external-cb n a b)))
:hints (("Goal" :use (:instance |+N+0=N|))))


(defthm zero-cb+n+0
  (implies (integerp n)
	   (equal (zero-cb (+ N 0))
		  (zero-cb n )))
:hints (("Goal" :use (:instance |+N+0=N|))))

(defthm inverse-cb+n+0
  (implies (integerp n)
	   (equal (inverse-cb (+ N 0) a )
		  (inverse-cb n a )))
:hints (("Goal" :use (:instance |+N+0=N|))))

(defthm inv-n-d-ca+1+n-2
  (implies (and (inv-ca (+ 1 n) a)
		(integerp n))
	   (inv-ca n (d-ca (+ n 1) a)))
  :hints (("Goal" :use ((:instance inv-n-d-ca+1+n-help (n (+ 1 n)))
			(:instance |+1+N-1=N|)))))

(defthm inv-ca+n+0
  (implies (integerp n)
	   (equal (inv-ca (+ N 0) a )
		  (inv-ca n a )))
:hints (("Goal" :use (:instance |+N+0=N|))))


(defthm zero-ca-1+n+1
  (implies (integerp n)
	   (equal (zero-ca (+ -1 N 1))
		  (zero-ca n )))
:hints (("Goal" :use (:instance |-1+N+1=N|))))

(defthm i-1+n
  (implies (integerp n)
	   (equal (i (+ -1 n) a)
		  (i (+ n -1) a)))
  :hints (("Goal" :use (:instance |-1+N=N-1|))))

(defthm zero-cb+-1+n
  (implies (integerp n)
	   (equal (zero-cb (+ N -1) )
		  (zero-cb (+ -1 n))))
  :hints (("Goal" :use (:instance |-1+N=N-1|))))

(defthm j+1+n
  (implies (integerp n)
	   (equal (j (+ 1 n) a)
		  (j (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))

(defthm zero-ca+-1+n+2
  (implies (integerp n)
	   (equal (zero-ca (+ -1 N 2) )
		  (zero-ca (+ n 1))))
  :hints (("Goal" :use (:instance |-1+N=N-1| (n (+ n 2))))))

(defthm rho+1+n
  (implies (integerp n)
	   (equal (rho (+ 1 n) a)
		  (rho (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm group-operation-cc+1+n
  (implies (integerp n)
	   (equal (group-operation-c_c (+ 1 n) a b)
		  (group-operation-c_c (+ n 1) a b)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm zero-cc+1+n
  (implies (integerp n)
	   (equal (ZERO-C_C (+ 1 N))
		  (ZERO-C_c (+ N 1))))
  :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)))))

(defthm zero-cb+1+n
  (implies (integerp n)
	   (equal (ZERO-Cb (+ 1 N))
		  (ZERO-Cb (+ N 1))))
  :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)))))

(defthm zero-cb+n+2
  (implies (integerp n)
	   (equal (ZERO-Cb (+ 1 1 N))
		  (ZERO-Cb (+ N 2))
		  ))
  :hints (("Goal" 
	   :use ((:instance |+1+N=N+1|)
		 (:instance |+1+N=N+1| (n (+ n 1)))))))

(defthm inverse-zero-cb-1+n
  (implies (integerp n)
	   (equal (INVERSE-CB (+ N -1) (ZERO-Cb (+ -1 N)))
		  (ZERO-Cb (+ -1 n))))
  :hints (("Goal" :in-theory (disable ZERO-CB+-1+N)
	   :use ((:instance |-1+N=N-1|)))))




(defthm group-operation-cb-change-1
  (implies (and (inv-cb n a)
		(inv-cb n b)
		(inv-cb n c)
		(integerp n)
		(equal (group-operation-cb n a b) c))
	   (equal (group-operation-cb n c (inverse-cb n b))
		  a)))


(defthm group-operation-cb-change-2
  (implies (and (inv-cb n a)
		(inv-cb n b)
		(inv-cb n c)
		(integerp n)
		(equal (group-operation-cb n a b) c))
	   (equal (group-operation-cb n c (inverse-cb n a))
		  b))
  :hints (("Goal" :use ((:instance group-operation-cb-commutativity)))))


(defthm sigma-j=gnrt-i-rho
  (implies (and (inv-cb n gnrt)
		(integerp n))
	   (equal (sigma n (j n gnrt))
		  (group-operation-cb n gnrt (i n (rho n gnrt)))
		  ))
  :hints (("Goal" :use ((:instance I-RHO+SIGMA-J)
			(:instance group-operation-cb-change-2
				   (a (i n (rho n gnrt)))
				   (b (sigma n (j n gnrt)))
				   (c gnrt))))))

(encapsulate 
 ()
 
(local
(defthm sigma-inverse-cb-d-cb....-1
  (implies (and (inv-ca (+ n 1) gnrt)
		(integerp n))
	   (equal (group-operation-cb n (sigma n (d-ca (+ n 1) gnrt))
				      (inverse-cb n (d-cb (+ n 1) (sigma (+ n 1) gnrt))))
		  (group-operation-cb n (sigma n (d-ca (+ n 1) gnrt))
				      (inverse-cb n (group-operation-cb n
								       (i n (rho n (d-cb (+ n 1) (sigma (+ n 1) gnrt))))
								       (sigma n (j n (d-cb (+ n 1) (sigma (+ n 1) gnrt)))))))))
  :hints (("Goal" :use (:instance i-rho+sigma-j (a (d-cb (+ n 1) (sigma (+ n 1) gnrt))))))
  ))

(local
(defthm sigma-inverse-cb-d-cb....-2
  (implies (and (inv-ca (+ n 1) gnrt)
		(integerp n))
	   (equal (group-operation-cb n (sigma n (d-ca (+ n 1) gnrt))
				      (inverse-cb n (d-cb (+ n 1) (sigma (+ n 1) gnrt))))
		  (group-operation-cb n (sigma n (d-ca (+ n 1) gnrt))
				      (group-operation-cb n 
							  (inverse-cb n (i n (rho n (d-cb (+ n 1) (sigma (+ n 1) gnrt)))))
							  (inverse-cb n (sigma n (j n (d-cb (+ n 1) (sigma (+ n 1) gnrt)))))))))
  :hints (("Goal" :use (:instance sigma-inverse-cb-d-cb....-1)))
  ))

(local
(defthm d-ca-j
  (implies (and (inv-cb n a)
		(integerp n))
	   (equal (j (+ n -1) (d-cb n a))
		  (d-ca n (j n a)))))
)

(local
(defthm d-ca-j+n+1
  (implies (and (inv-cb (+ n 1) a)
		(integerp n))
	   (equal (j n (d-cb (+ n 1) a))
		  (d-ca (+ n 1) (j (+ n 1) a))))
  :hints (("Goal" :use ((:instance d-ca-j (n (+ n 1)))
			(:instance |+N+0=N|)))))
)

(local
(defthm sigma-inverse-cb-d-cb....-3
  (implies (and (inv-ca (+ n 1) gnrt)
		(integerp n))
	   (equal (group-operation-cb n (sigma n (d-ca (+ n 1) gnrt))
				      (inverse-cb n (d-cb (+ n 1) (sigma (+ n 1) gnrt))))
		  (group-operation-cb n (sigma n (d-ca (+ n 1) gnrt))
				      (group-operation-cb n 
							  (inverse-cb n (i n (rho n (d-cb (+ n 1) (sigma (+ n 1) gnrt)))))
							  (inverse-cb n (sigma n (d-ca (+ n 1) (j (+ n 1) (sigma (+ n 1) gnrt)))))))))
  :hints (("Goal" :use (:instance sigma-inverse-cb-d-cb....-2)))
  )
)

(local
(defthm sigma-inverse-cb-d-cb....-4
  (implies (and (inv-ca (+ n 1) gnrt)
		(integerp n))
	   (equal (group-operation-cb n (sigma n (d-ca (+ n 1) gnrt))
				      (inverse-cb n (d-cb (+ n 1) (sigma (+ n 1) gnrt))))
		  (group-operation-cb n (sigma n (d-ca (+ n 1) gnrt))
				      (group-operation-cb n 
							  (inverse-cb n (i n (rho n (d-cb (+ n 1) (sigma (+ n 1) gnrt)))))
							  (inverse-cb n (sigma n (d-ca (+ n 1) gnrt)))))))
  :hints (("Goal" :use (:instance sigma-inverse-cb-d-cb....-3)))
  ))

(local
(defthm remove-group-operation-cb
  (implies (and (inv-cb n a)
		(inv-cb n b)
		(integerp n))
	   (equal (group-operation-cb n a (group-operation-cb n b (inverse-cb n a)))
		  b))
  :hints (("Goal" :use (:instance group-operation-cb-commutativity (a a) (b (group-operation-cb n b (inverse-cb n a)))))))
)


(defthm sigma-inverse-cb-d-cb....-5
  (implies (and (inv-ca (+ n 1) gnrt)
		(integerp n))
	   (equal (group-operation-cb n (sigma n (d-ca (+ n 1) gnrt))
				      (inverse-cb n (d-cb (+ n 1) (sigma (+ n 1) gnrt))))
		  (inverse-cb n (i n (rho n (d-cb (+ n 1) (sigma (+ n 1) gnrt)))))))
  :hints (("Goal" :use ((:instance sigma-inverse-cb-d-cb....-4)
			(:instance remove-group-operation-cb
				   (a (sigma n (d-ca (+ n 1) gnrt)))
				   (b (inverse-cb n (i n (rho n (d-cb (+ n 1) (sigma (+ n 1) gnrt))))))))))
  )
)

(defthm remove-group-operation-cc
  (implies (and (inv-c_c n a)
		(inv-c_c n b)
		(integerp n))
	   (equal (group-operation-c_c n a (group-operation-c_c n (inverse-c_c n a) b))
		  b))
  :hints (("Goal" :use ((:instance group-operation-cc-commutativity (a (inverse-c_c n a)))
			(:instance group-operation-cC-commutativity (a a) (b (group-operation-c_c n b (inverse-c_c n a)))))))
  )



(defthm lemma-prop2-1
  (implies (and (inv-ca (+ n 1) a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ N -1)
		   (inverse-c_c (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))
		   (rho (+ N -1) (d-cb n (sigma n (d-ca (+ n 1) a))))
		   )
		  (group-operation-c_c
		   (+ N -1)
		   (inverse-c_c (+ N -1) (rho (+ N -1) (i (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))))
		   (rho (+ N -1) (d-cb n (sigma n (d-ca (+ n 1) (j (+ n 1) (sigma (+ n 1) a))))))
		   ))))



(defthm d-ca-j
  (implies (and (inv-cb n a)
		(integerp n))
	   (equal (j (+ n -1) (d-cb n a))
		  (d-ca n (j n a))))
  :rule-classes nil)



(defthm d-ca-j+n+1
  (implies (and (inv-cb (+ n 1) a)
		(integerp n))
	   (equal (j n (d-cb (+ n 1) a))
		  (d-ca (+ n 1) (j (+ n 1) a))))
  :hints (("Goal" :use ((:instance d-ca-j (n (+ n 1)))
			(:instance |+N+0=N|))))
  :rule-classes nil)

(defthm inverse-c_c-inverse-c_c
  (implies (and (inv-c_c (+ n -1) a)
		(integerp n))
	   (equal (inverse-c_c (+ n -1)
			       (inverse-c_c (+ n -1) a))
		  a)))

(defthm lemma-prop2-2-a
  (implies (and (inv-ca (+ n 1) a)
		(integerp n))
	   (equal 
	    (inverse-c_c (+ N -1) (rho (+ N -1) (i (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))))
	    (inverse-c_c (+ N -1) (rho (+ N -1) (inverse-cb (+ N -1) (i (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))))))
	   )
  :hints (("Goal" :in-theory (disable lemma-prop2-1)
	   :use ((:instance i=inverse-i
			    (n (+ N -1))
			    (c (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a))))))
		  ))))


(defthm lemma-prop2-2-b
  (implies (and (inv-ca (+ n 1) a)
		(integerp n))
	   (equal 
	    (inverse-c_c (+ N -1) (rho (+ N -1) (i (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))))
	    (inverse-c_c (+ N -1) (inverse-c_c (+ N -1) (rho (+ N -1) (i (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))))))
	   )
  :hints (("Goal" :in-theory (disable I=INVERSE-I)
	   :use ((:instance lemma-prop2-2-a)))))


(defthm lemma-prop2-2-c
  (implies (and (inv-ca (+ n 1) a)
		(integerp n))
	   (equal 
	    (inverse-c_c (+ N -1) (rho (+ N -1) (i (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))))
	    (rho (+ N -1) (i (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))))
	   )
  :hints (("Goal" :in-theory (disable I=INVERSE-I)
	   :use ((:instance lemma-prop2-2-b)))))



(defthm lemma-prop2-2
  (implies (and (inv-ca (+ n 1) a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ N -1)
		   (inverse-c_c (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))
		   (rho (+ N -1) (d-cb n (sigma n (d-ca (+ n 1) a))))
		   )
		  (group-operation-c_c
		   (+ N -1)
		   (rho (+ N -1) (d-cb n (i n (rho n (d-cb (+ n 1) (sigma (+ n 1) a))))))
		   (rho (+ N -1) (d-cb n (sigma n (j n (d-cb (+ n 1) (sigma (+ n 1) a))))))
		   )))
  :hints (("Goal" :in-theory (disable lemma-prop2-1)
	   :use ((:instance lemma-prop2-1)
		 (:instance lemma-prop2-2-c)
		 (:instance d-ca-j+n+1 (a (sigma (+ n 1) a)))))))



(defthm lemma-prop2-3
  (implies (and (inv-ca (+ n 1) a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ N -1)
		   (inverse-c_c (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))
		   (rho (+ N -1) (d-cb n (sigma n (d-ca (+ n 1) a))))
		   )
		  (rho (+ N -1) (d-cb n 
				      (group-operation-cb
				       n
				       (i n (rho n (d-cb (+ n 1) (sigma (+ n 1) a))))
				       (sigma n (j n (d-cb (+ n 1) (sigma (+ n 1) a))))
				       )))
		    ))
  :hints (("Goal" :in-theory (disable lemma-prop2-1)
	   :use ((:instance lemma-prop2-2)
		 ))))


(defthm lemma-prop2-4
  (implies (and (inv-ca (+ n 1) a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ N -1)
		   (inverse-c_c (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))
		   (rho (+ N -1) (d-cb n (sigma n (d-ca (+ n 1) a))))
		   )
		  (rho (+ N -1) (d-cb n (d-cb (+ n 1) (sigma (+ n 1) a))
				      ))
		    ))
  :hints (("Goal" :in-theory (disable lemma-prop2-1)
	   :use ((:instance lemma-prop2-3)
		 (:instance i-rho+sigma-j (a (d-cb (+ n 1) (sigma (+ n 1) a))))
		 ))))


(defthm zero-d-cb-d-cb-1
  (implies (and (inv-cb n a)
		(integerp n))
	   (equal (D-CB (+ N -1) (D-CB n a))
		  (zero-cb (+ (+ N -1) -1))))
  :rule-classes nil)

(defthm zero-d-cb-d-cb
  (implies (and (inv-cb (+ n 1) a)
		(integerp n))
	   (equal (D-CB N (D-CB (+ N 1) a))
		  (zero-cb (+ N -1))))
  :hints (("Goal" :use ((:instance zero-d-cb-d-cb-1 (n (+ N 1))))))
  :rule-classes nil)


(defthm rho-zero-cb
  (implies (integerp n)
	   (EQUAL (RHO (+ N -1) (ZERO-CB (+ -1 N)))
		  (ZERO-C_C (+ N -1))))
   :hints (("Goal" :in-theory (disable ZERO-CB+-1+N)
	   :use ((:instance |-1+N=N-1|)))))
  

(defthm lemma-prop2-5
  (implies (and (inv-ca (+ n 1) a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ N -1)
		   (inverse-c_c (+ N -1) (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))
		   (rho (+ N -1) (d-cb n (sigma n (d-ca (+ n 1) a))))
		   )
		  (zero-c_c (+ N -1))
		    ))
  :hints (("Goal" :in-theory (disable lemma-prop2-1)
	   :use ((:instance lemma-prop2-4)
		 (:instance zero-d-cb-d-cb (a (sigma (+ n 1) a)))))))



(defthm group-operation-cc-inverse-change-1
  (implies (and (inv-c_c n a)
		(inv-c_c n b)
		(integerp n)
		(equal (group-operation-c_c n (inverse-c_c n a) b)
		       (zero-c_c n)))
	   (equal (group-operation-c_c n (group-operation-c_c n (inverse-c_c n a) b) a)
		  a))
  :rule-classes nil)

(defthm group-operation-cc-inverse-change-2
  (implies (and (inv-c_c n a)
		(inv-c_c n b)
		(integerp n)
		)
	   (equal (group-operation-c_c n (group-operation-c_c n (inverse-c_c n a) b) a)
		  b))
  :rule-classes nil)

(defthm group-operation-cc-inverse-change
  (implies (and (inv-c_c n a)
		(inv-c_c n b)
		(integerp n)
		(equal (group-operation-c_c n (inverse-c_c n a) b)
		       (zero-c_c n)))
	   (equal b a))
  :hints (("Goal" :use ((:instance group-operation-cc-inverse-change-1)
			(:instance group-operation-cc-inverse-change-2))))
  :rule-classes nil
)
	   
(defthm group-operation-cc-inverse-change-result
  (implies (and (inv-ca (+ n 1) a)
	       (integerp n)) 		
	   (equal (rho (+ N -1) (d-cb n (sigma n (d-ca (+ n 1) a))))
		  (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))) ))
  :hints (("Goal" :use ((:instance lemma-prop2-5)
			(:instance group-operation-cc-inverse-change
				   (n (+ N -1))
				   (a (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) a)))))
				   (b (rho (+ N -1) (d-cb n (sigma n (d-ca (+ n 1) a))))))
			))))


;;;**************************************************
;;;
;;; Definition of the Reduction Cone(j) =>> CC
;;;
;;;**************************************************


(defreduction 
   inv-ring-R addition-ring-R zero-element-R inverse-R product-ring-R unit-R
   inv-CONE-CONE-C2-C1-CONE-SES3 group-operation-CONE-CONE-C2-C1-CONE-SES3
   zero-CONE-CONE-C2-C1-CONE-SES3 external-CONE-CONE-C2-C1-CONE-SES3
   inverse-CONE-CONE-C2-C1-CONE-SES3 d-CONE-CONE-C2-C1-CONE-SES3
   inv-C_C group-operation-C_C zero-C_C external-C_C inverse-C_C d-C_C 
   f-cone-C  g-cone-C h-cone-cone 
   cone->C
   )



;;;**************************************************
;;;
;;; Definition of the new Reduction 
;;; Cone(dj) =>> CC  (Cone(dj) =>> Cone(j) =>> CC) 
;;;
;;;**************************************************


;(include-book "SES3-Theorem-help")

(include-book "cmps-reductions-structure")


(defthm property1
  (IMPLIES (AND (INV-CB N a)
              (INV-CB N b)
              (INV-CB N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-CB N a (GROUP-OPERATION-CB N b c))
		(GROUP-OPERATION-CB N c (GROUP-OPERATION-CB N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-cb-commutativity
				   (a c)
				   (b (GROUP-OPERATION-CB N a b)))))))



(defthm property2
  (IMPLIES (AND (INV-C_c N a)
              (INV-C_c N b)
              (INV-C_c N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C_C N a (GROUP-OPERATION-C_c N b c))
		(GROUP-OPERATION-C_C N c (GROUP-OPERATION-C_c N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-cc-commutativity
				   (a c)
				   (b (GROUP-OPERATION-C_c N a b)))))))


(defthm property3
  (IMPLIES (AND 
	    (INV-ca N a)
              (INV-ca N b)
              (INV-ca N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-CA N a (GROUP-OPERATION-ca N b c))
		(GROUP-OPERATION-CA N c (GROUP-OPERATION-ca N a b))))
  )
  

(DEFTHM GROUP-OPERATION-dB-COMMUTATIVITY
                      (IMPLIES (AND (INV-dB N A)
                                    (INV-dB N B)
                                    (INTEGERP N))
                               (EQUAL (GROUP-OPERATION-dB N A B)
                                      (GROUP-OPERATION-dB N B A)))
                      :RULE-CLASSES NIL)

(defthm property1-db
  (IMPLIES (AND (INV-DB N a)
              (INV-DB N b)
              (INV-DB N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-DB N a (GROUP-OPERATION-DB N b c))
		(GROUP-OPERATION-DB N c (GROUP-OPERATION-DB N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-db-commutativity
				   (a c)
				   (b (GROUP-OPERATION-dB N a b)))))))

(DEFTHM GROUP-OPERATION-hB-COMMUTATIVITY
                      (IMPLIES (AND (INV-hB N A)
                                    (INV-hB N B)
                                    (INTEGERP N))
                               (EQUAL (GROUP-OPERATION-hB N A B)
                                      (GROUP-OPERATION-hB N B A)))
                      :RULE-CLASSES NIL)

(defthm property1-hb
  (IMPLIES (AND (INV-hB N a)
              (INV-hB N b)
              (INV-hB N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-hB N a (GROUP-OPERATION-hB N b c))
		(GROUP-OPERATION-hB N c (GROUP-OPERATION-hB N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-hb-commutativity
				   (a c)
				   (b (GROUP-OPERATION-hB N a b)))))))


(DEFTHM GROUP-OPERATION-da-COMMUTATIVITY
                      (IMPLIES (AND (INV-da N A)
                                    (INV-da N B)
                                    (INTEGERP N))
                               (EQUAL (GROUP-OPERATION-da N A B)
                                      (GROUP-OPERATION-da N B A)))
                      :RULE-CLASSES NIL)

(defthm property1-da
  (IMPLIES (AND (INV-Da N a)
              (INV-Da N b)
              (INV-Da N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-Da N a (GROUP-OPERATION-Da N b c))
		(GROUP-OPERATION-Da N c (GROUP-OPERATION-Da N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-da-commutativity
				   (a c)
				   (b (GROUP-OPERATION-da N a b)))))))

(DEFTHM GROUP-OPERATION-ha-COMMUTATIVITY
                      (IMPLIES (AND (INV-ha N A)
                                    (INV-ha N B)
                                    (INTEGERP N))
                               (EQUAL (GROUP-OPERATION-ha N A B)
                                      (GROUP-OPERATION-ha N B A)))
                      :RULE-CLASSES NIL)

(defthm property1-ha
  (IMPLIES (AND (INV-ha N a)
              (INV-ha N b)
              (INV-ha N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-ha N a (GROUP-OPERATION-ha N b c))
		(GROUP-OPERATION-ha N c (GROUP-OPERATION-ha N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-ha-commutativity
				   (a c)
				   (b (GROUP-OPERATION-ha N a b)))))))


(defthm d-da+1+n
  (implies (integerp n)
	   (equal (d-da (+ 1 n) a)
		  (d-da (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))



(defthm inv-da+1+n-1
  (implies (integerp n)
	   (equal (inv-da (+ 1 n -1) a)
		  (inv-da n a)))
  :hints (("Goal" :use ((:instance |+1+N-1=N|)
			))))

(DEFTHM INV-N-D-dA+1+N-HELP
  (IMPLIES (AND (INV-dA N A) (INTEGERP N))
	   (INV-dA (+ N -1) (D-dA N A))))

(defthm inv-n-d-da+1+n-2
  (implies (and (inv-da (+ 1 n) a)
		(integerp n))
	   (inv-da n (d-da (+ n 1) a)))
  :hints (("Goal" :use ((:instance inv-n-d-da+1+n-help (n (+ 1 n)))
			(:instance |+1+N-1=N|)))))


(defthm inverse-db-1+n
  (implies (integerp n)
	   (equal (inverse-db (+ -1 n) a)
		  (inverse-db (+ n -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)))))



(defthm group-operation-da+1+n-1
  (implies (integerp n)
	   (equal (group-operation-da (+ 1 N -1) a b)
		  (group-operation-da n a b)))
  :hints (("Goal" :use ((:instance |+1+N-1=N|)
			))))


(defthm group-operation-da+1+n
  (implies (integerp n)
	   (equal (group-operation-da (+ 1 N) a b)
		  (group-operation-da (+ n 1) a b)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))


(defthm inv-da+1+n
  (implies (integerp n)
	   (equal (inv-da (+ 1 N) a)
		  (inv-da (+ n 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))


(defthm inv-da+n+0
  (implies (integerp n)
	   (equal (inv-da (+ N 0) a)
		  (inv-da n a)))
  :hints (("Goal" :use ((:instance |+N+0=N|)
			))))

(defthm external-da+1+n
  (implies (integerp n)
	   (equal (external-da (+ 1 N) a b)
		  (external-da (+ n 1) a b)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))

(defthm inverse-da+1+n
  (implies (integerp n)
	   (equal (inverse-da (+ 1 N)  b)
		  (inverse-da (+ n 1) b)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))

(defthm zero-da+1+n
  (implies (integerp n)
	   (equal (zero-da (+ 1 N) )
		  (zero-da (+ n 1) )))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))


(defthm external-da+n+0
  (implies (integerp n)
	   (equal (external-da (+ N 0) a b)
		  (external-da n a b)))
  :hints (("Goal" :use ((:instance |+N+0=N|)
			))))

(defthm inverse-da+n+0
  (implies (integerp n)
	   (equal (inverse-da (+ N 0)  b)
		  (inverse-da n b)))
  :hints (("Goal" :use ((:instance |+N+0=N|)
			))))

(defthm zero-da+n+0
  (implies (integerp n)
	   (equal (zero-da  (+ N 0))
		  (zero-da n )))
  :hints (("Goal" :use ((:instance |+N+0=N|)
			))))

(defthm group-operation-da+n+0
  (implies (integerp n)
	   (equal (group-operation-da (+ N 0) a b)
		  (group-operation-da n a b)))
  :hints (("Goal" :use ((:instance |+N+0=N|)
			))))



(defthm group-operation-da-1+n
  (implies (integerp n)
	   (equal (group-operation-da (+ -1 N) a b)
		  (group-operation-da (+ n -1) a b)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)
			))))


(defthm d-da-1+n+1
  (implies (integerp n)
	   (equal (d-da (+ -1 N 1) a)
		  (d-da n a)))
  :hints (("Goal" :use ((:instance |-1+N+1=N|)
			))))


(defthm lga-1+n
  (implies (integerp n)
	   (equal (lga (+ -1 N) a)
		  (lga (+ N -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)
			))))


(defthm lfb-1+n
  (implies (integerp n)
	   (equal (lfb (+ -1 N) a)
		  (lfb (+ N -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)
			))))


(defthm zero-da-1-1+n+1
  (implies (integerp n)
	   (equal (ZERO-DA (+ -1 -1 N 1))
		  (ZERO-DA (+ N -1))))
    :hints (("Goal" :use ((:instance |-1+N=N-1| (n (+ n 1))) 
			  (:instance |-1+N=N-1| (n (+ n 0)))
			))))



(defthm zero-d-da-d-da-1
  (implies (and (inv-da n a)
		(integerp n))
	   (equal (D-da (+ -1 n) (D-da n a))
		  (zero-da (+ -1 (+ -1 n)))))
  :hints (("Goal" :in-theory (disable ASSOCIATIVITY-OF-+)))
  :rule-classes nil)

(defthm zero-d-da-d-da
  (implies (and (inv-da (+ n 1) a)
		(integerp n))
	   (equal (D-da N (D-da (+ N 1) a))
		  (zero-da (+ N -1))))
  :hints (("Goal" :use ((:instance zero-d-da-d-da-1 (n (+ N 1))))))
  )


(defthm zero-db-1-1+n
  (implies (integerp n)
	   (equal (ZERO-DB (+ -1 -1 N))
		  (ZERO-DB (+ N -2))))
  :hints (("Goal" :use ((:instance |-1-1+N=N-2|)
			))))


(defthm d-db-1+n
  (implies (integerp n)
	   (equal (d-db (+ -1 n) a)
		  (d-db (+ n -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)))))


(defthm zero-d-db-d-db-1
  (implies (and (inv-db n a)
		(integerp n))
	   (equal (D-db (+ -1 n) (D-db n a))
		  (zero-db (+ -1 (+ -1 n)))))
  :hints (("Goal" :in-theory (disable  d-db-1+n ASSOCIATIVITY-OF-+)))
  :rule-classes nil)

(defthm zero-d-db-d-db
  (implies (and (inv-db n a)
		(integerp n))
	   (equal (D-db (+ n -1) (D-db n a))
		  (zero-db (+ N -2))))
  :hints (("Goal" :use ((:instance zero-d-db-d-db-1))))
  )


(defthm lfa-1+n
  (implies (integerp n)
	   (equal (lfa (+ 1 N) a)
		  (lfa (+ N 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))

(defthm lfa-1+n+1
  (implies (integerp n)
	   (equal (lfa (+ -1 N 1) a)
		  (lfa n a)))
  :hints (("Goal" :use ((:instance |-1+N+1=N|)
			))))


(defthm lha-1+n
  (implies (integerp n)
	   (equal (lha (+ 1 N) a)
		  (lha (+ N 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))


(defthm inv-da-lha
  (implies (and (inv-da n a)
		(integerp n))
	   (inv-da (+ 1 n) (lha n a))))



(defthm inv-da-lha+n+1
  (implies (and (inv-da (+ N 1) a)
		(integerp n))
	   (inv-da (+ n 2) (lha (+ N 1) a)))
  :hints (("Goal" :use ((:instance inv-da-lha (n (+ N 1)))
			(:instance |+1+N=N+1| (n (+ n 1)))
			))))
		

(defthm inverse-db+1+n
  (implies (integerp n)
	   (equal (inverse-db (+ 1 N)  b)
		  (inverse-db (+ n 1) b)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))


(defthm lga+1+n
  (implies (integerp n)
	   (equal (lga (+ 1 N) a)
		  (lga (+ N 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))


(defthm lga+n+0
  (implies (integerp n)
	   (equal (lga (+ N 0) a)
		  (lga n a)))
  :hints (("Goal" :use ((:instance |+N+0=N|)
			))))

(defthm lgb-1+n
  (implies (integerp n)
	   (equal (lgb (+ -1 n) a)
		  (lgb (+ n -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)))))

(defthm lfb+1+n
  (implies (integerp n)
	   (equal (lfb (+ 1 N) a)
		  (lfb (+ N 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))

(defthm lha-1+n+1
  (implies (integerp n)
	   (equal (lha (+ -1 N 1) a)
		  (lha n a)))
  :hints (("Goal" :use ((:instance |-1+N+1=N|)
			))))



(defthm group-operation-da-zero-da
  (implies (and (inv-da (+ n 1) a)
		(integerp n))
	   (equal (GROUP-OPERATION-DA (+ N 1)
                                  (ZERO-DA (+ N 1))
                                  a)
		  a)))


(defthm inv-d-da+n+2-help
  (implies (and (inv-da n a)
		(integerp n))
	   (inv-da (+ n -1) (D-DA n a)))
  :rule-classes nil)

(defthm inv-d-da+n+2
  (implies (and (inv-da (+ n 2) a)
		(integerp n))
	   (inv-da (+ n 1) (D-DA (+ N 2) a)))
  :hints (("Goal" :use (:instance inv-d-da+n+2-help
				  (n (+ N 2))))))


(defthm group-operation-da-zero-da-b
  (implies (and (inv-da (+ n 1) a)
		(integerp n))
	   (equal (GROUP-OPERATION-DA (+ N 1)
				      a
				      (ZERO-DA (+ N 1))
                                  )
		  a)))


(defthm lfb-lhb-n
  (implies (and (inv-db n a)
		(integerp n))
	   (equal (LFB (+ 1 n) (LHB N a))
		  (zero-cb (+ 1 n))))
  :hints (("Goal" :in-theory (disable LFB+1+N ZERO-CB+1+N ))))

(defthm lfb-lhb-n2
  (implies (and (inv-db n a)
		(integerp n))
	   (equal (LFB (+ n 1) (LHB N a))
		  (zero-cb (+ n 1))))
 :hints (("Goal" :in-theory (disable LFB+1+N ZERO-CB+1+N )
	  :use ((:instance lfb-lhb-n)
		(:instance |+1+N=N+1|)))))


(defthm reduction-property-la-help
  (implies (and (inv-da n a)
		(integerp n))
	   (EQUAL (GROUP-OPERATION-DA n
                               (LHA (+ -1 n) (D-DA n a))
                               (D-DA (+ 1 n) (LHA n a)))
           (GROUP-OPERATION-DA n
                               a
                               (INVERSE-DA n
                                           (LGA n
                                                (LFA n a))))))
 :hints (("Goal" :in-theory (disable D-DA+1+N))))


(defthm reduction-property-la
  (implies (and (inv-da (+ N 1)  a)
		(integerp n))
	   (EQUAL (GROUP-OPERATION-DA (+ N 1)
                               (LHA N (D-DA (+ N 1) a))
                               (D-DA (+ N 2) (LHA (+ N 1) a)))
           (GROUP-OPERATION-DA (+ N 1)
                               a
                               (INVERSE-DA (+ N 1)
                                           (LGA (+ N 1)
                                                (LFA (+ N 1) a))))))
 :hints (("Goal" 
	  :use ((:instance reduction-property-la-help (n (+ n 1)))))))


(defthm lhb-1+n
  (implies (integerp n)
	   (equal (lhb (+ -1 n) a)
		  (lhb (+ n -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)))))


(defthm inverse-db+n+0
  (implies (integerp n)
	   (equal (inverse-db (+ N 0) a)
		  (inverse-db n a)))
  :hints (("Goal" :use ((:instance |+N+0=N|)
			))))

(defthm d-db+1+n
  (implies (integerp n)
	   (equal (d-db (+ 1 N) a)
		  (d-db (+ N 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))



(defthm inv-db-lhb
  (implies (and (inv-db n a)
		(integerp n))
	   (inv-db (+ n 1) (lhb n a))))



(defthm inv-db-lhb+n+1
  (implies (and (inv-db (+ N -1) a)
		(integerp n))
	   (inv-db n (lhb (+ N -1) a)))
  :hints (("Goal" :use ((:instance inv-db-lhb (n (+ N -1)))
			(:instance |+N+0=N|)
			))))

(defthm inv-d-db+n+1-help
  (implies (and (inv-db n a)
		(integerp n))
	   (inv-db (+ n -1) (D-Db n a)))
  :rule-classes nil)

(defthm inv-d-db+n+1
  (implies (and (inv-db (+ n 1) a)
		(integerp n))
	   (inv-db n (D-Db (+ N 1) a)))
  :hints (("Goal" :use ((:instance inv-d-db+n+1-help (n (+ N 1)))
			(:instance |+N+0=N|)))))


(defthm inverse-inverse-db
  (implies (and (inv-db n a)
		(integerp n))
	   (equal (inverse-db n (inverse-db n a))
		  a)))


(defthm reduction-property-lb-help
  (implies (and (inv-db n a)
		(integerp n))
	   (EQUAL (GROUP-OPERATION-Db n
                               (LHb (+ -1 n) (D-Db n a))
                               (D-Db (+ 1 n) (LHb n a)))
           (GROUP-OPERATION-Db n
                               a
                               (INVERSE-Db n
                                           (LGb n
                                                (LFb n a))))))
 :hints (("Goal" :in-theory (disable  LHB-1+N D-Db+1+N))))

(defthm reduction-property-lb
  (implies (and (inv-db n a)
		(integerp n))
	   (EQUAL (GROUP-OPERATION-Db n
                               (LHb (+ n -1) (D-Db n a))
                               (D-Db (+ n 1) (LHb n a)))
           (GROUP-OPERATION-Db n
                               a
                               (INVERSE-Db n
                                           (LGb n
                                                (LFb n a))))))
 :hints (("Goal" :use (:instance reduction-property-lb-help))))



(defthm lfa-lha-n
  (implies (and (inv-da n a)
		(integerp n))
	   (equal (LFa (+ 1 n) (LHa N a))
		  (zero-ca (+ 1 n))))
  :hints (("Goal" :in-theory (disable LFA-1+N ZERO-Ca+1+N ))))


(defthm lfa-lha-n2
  (implies (and (inv-da n a)
		(integerp n))
	   (equal (LFa (+ n 1) (LHa N a))
		  (zero-ca (+ n 1))))
  :hints (("Goal" :in-theory (disable LFA-1+N ZERO-Ca+1+N )
	   :use ((:instance lfa-lha-n)
		 (:instance |+1+N=N+1|)))))

(defthm lfa-lha-n3
  (implies (and (inv-da (+ n 1) a)
		(integerp n))
	   (equal (LFa (+ n 2) (LHa (+ n 1) a))
		  (zero-ca (+ n 2))))
 :hints (("Goal" :in-theory (disable LFA-1+N ZERO-Ca+1+N
				     LHA-1+N INV-DA+1+N) 
	  :use ((:instance lfa-lha-n2 (n (+ n 1)))
		))))


(defthm zero-db+1+n
  (implies (integerp n)
	   (equal (zero-db (+ 1 N) )
		  (zero-db (+ N 1) )))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))


(defthm lha-lha-n
  (implies (and (inv-da n a)
		(integerp n))
	   (equal (LHA (+ 1 N) (LHA n a))
		  (ZERO-DA (+ 1 (+ 1 n)))))
  :hints (("Goal" :in-theory (disable LhA-1+N ZERO-da+1+N ))))



(defthm lhb+1+n
  (implies (integerp n)
	   (equal (lhb (+ 1 N) a)
		  (lhb (+ N 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)
			))))


(defthm inverse-db-inverse-db+n+2
  (implies (and (inv-db (+ n 2) a)
		(integerp n))
	   (equal (inverse-db (+ n 2) (inverse-db (+ n 2) a))
		  a)))




(defthm inv-db-lhb+n+1-2
  (implies (and (inv-db (+ N 1) a)
		(integerp n))
	   (inv-db (+ n 2) (lhb (+ N 1) a)))
  :hints (("Goal" :use ((:instance inv-db-lhb (n (+ N 1)))
			(:instance |+1+N=N+1| (n (+ n 1)))
			))))


(defthm lhb-lhb-n
  (implies (and (inv-db n a)
		(integerp n))
	   (equal (LHb (+ 1 N) (LHb n a))
		  (ZERO-Db (+ 1 (+ 1 n)))))
  :hints (("Goal" :in-theory (disable Lhb+1+N ZERO-db+1+N ))))


(defthm lhb-lhb-n2
  (implies (and (inv-db n a)
		(integerp n))
	   (equal (LHb (+ N 1) (LHb n a))
		  (ZERO-Db (+ n 2))))
  :hints (("Goal" :in-theory (disable Lhb+1+N ZERO-db+1+N )
	   :use ((:instance lhb-lhb-n)
		 (:instance |+1+N=N+1|)
		 (:instance |+1+N=N+1| (n (+ n 1)))))))




(definstance-*cmps*
  ((inv-ring-cmps inv-ring-R)
    (addition-ring-cmps addition-ring-R)
    (product-ring-cmps product-ring-R)
    (inverse-cmps inverse-R)
    (zero-element-cmps zero-element-R)
    (unit-cmps unit-R)
    (inv-top inv-CONE-CONE-D2-D1-CONE-SES3)
    (group-operation-top group-operation-CONE-CONE-D2-D1-CONE-SES3)
    (zero-top zero-CONE-CONE-D2-D1-CONE-SES3)
    (external-top external-CONE-CONE-D2-D1-CONE-SES3)
    (inverse-top inverse-CONE-CONE-D2-D1-CONE-SES3)
    (d-top d-CONE-CONE-D2-D1-CONE-SES3)
    (inv-middle inv-CONE-CONE-C2-C1-CONE-SES3) 
    (group-operation-middle group-operation-CONE-CONE-C2-C1-CONE-SES3)
    (zero-middle zero-CONE-CONE-C2-C1-CONE-SES3)
    (external-middle external-CONE-CONE-C2-C1-CONE-SES3)
    (inverse-middle inverse-CONE-CONE-C2-C1-CONE-SES3)
    (d-middle d-CONE-CONE-C2-C1-CONE-SES3)
    (inv-bottom inv-c_C) 
    (group-operation-bottom group-operation-c_c)
    (zero-bottom zero-c_c)
    (external-bottom external-c_c)
    (inverse-bottom inverse-c_c)
    (d-bottom d-c_c)
    (f1 f-cone-c)
    (g1 g-cone-c)
    (h1 h-cone-cone)
    (f2 lf-cones-cone-ses3)
    (g2 lg-cones-cone-ses3)
    (h2 lh-cones-cone-ses3)
    )
  "-cone-dj-cc")



;;;**************************************************
;;;
;;; Definition of the Equivalence: 
;;; CC <<= Cone(j) <<= Cone(dj) =>> Cone(hj)
;;;
;;;**************************************************


(defthm lfa+1+n
  (implies (integerp n)
	   (equal (lfa (+ -1 n) a)
		  (lfa (+ n -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)))))


(defthm lfa-d-da
  (implies (and (inv-da n a)
		(integerp n))
	   (equal (lfa (+ n -1) (d-da n a))
		  (d-ca n (lfa n a))))
  )


(defthm lfa-d-da+n+1+n+0
  (implies (and (inv-da (+ N 1) a)
		(integerp n))
	   (equal (lfa n (d-da (+ N 1) a))
		  (d-ca (+ N 1) (lfa (+ N 1) a))))
  :rule-classes nil
  :hints (("Goal" :use ((:instance |+N+0=N|)))))



(defthm group-operation-cc-inverse-change-result-2
  (implies (and (inv-da (+ n 1) a)
	       (integerp n)) 		
	   (equal (d-c_c n (rho n (d-cb (+ n 1) (sigma (+ n 1) (LFA (+ N 1) a)))))
		  (rho (+ N -1) (d-cb n (sigma n (d-ca (+ n 1) (LFA (+ N 1) a)))))
		   ))
  :hints (("Goal" :use ((:instance group-operation-cc-inverse-change-result
				   (a (LFA (+ N 1) a)))))))



(defthm lfa+n+0
  (implies (integerp n)
	   (equal (lfa (+ n 0) a)
		  (lfa n a)))
  :hints (("Goal" :use ((:instance |+N+0=N|)))))


(defthm lgb+1+n
  (implies (integerp n)
	   (equal (lgb (+ 1 n) a)
		  (lgb (+ n 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)))))


(defthm group-operation-db+1+n
  (implies (integerp n)
	   (equal (group-operation-db (+ 1 n) a b)
		  (group-operation-db (+ n 1) a b)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)))))


(defthm group-operation-zero-da-n+2
  (implies (and (inv-da (+ n 2) a)
		(integerp n))
	   (equal (group-operation-da (+ n 2) (zero-da (+ n 2)) a)
		  a)))

(defthm lgb-i-1
  (implies (and (inv-c_c n a)
		(integerp n))
	   (EQUAL (LGB N (I N A))
		  (LGB N  (INVERSE-cB N (I N A)))))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable i=inverse-i)
	   :use (:instance i=inverse-i (c a)))))


(defthm lgb-i
  (implies (and (inv-c_c n a)
		(integerp n))
	   (EQUAL (INVERSE-DB N (LGB N (I N A)))
		  (LGB N (I N A))
		  ))
  :hints (("Goal" :in-theory (disable i=inverse-i)
	   :use (:instance lgb-i-1))))


(defthm lgb-i
  (implies (and (inv-c_c n a)
		(integerp n))
	   (EQUAL (INVERSE-DB N (LGB N (I N A)))
		  (LGB N (I N A))
		  ))
  :hints (("Goal" :in-theory (disable i=inverse-i)
	   :use (:instance lgb-i-1))))


(defthm lgb+n+0
  (implies (integerp n)
	   (equal (lgb (+ n 0) a)
		  (lgb n a)))
  :hints (("Goal" :use ((:instance |+N+0=N|)))))


(defthm group-operation-db+n+0
  (implies (integerp n)
	   (equal (GROUP-OPERATION-DB (+ n 0) a b)
		  (GROUP-OPERATION-DB n a b)))
  :hints (("Goal" :use ((:instance |+N+0=N|)))))

(defthm group-operation-db-1+n-1
  (implies (integerp n)
	   (equal (GROUP-OPERATION-DB (+ -1 n 1) a b)
		  (GROUP-OPERATION-DB n a b)))
  :hints (("Goal" :use ((:instance |-1+N+1=N|)))))


(defthm inv-da-lha+n+2
  (implies (and (inv-da (+ N 2) a)
		(integerp n))
	   (inv-da (+ n 3) (lha (+ N 2) a)))
  :hints (("Goal" :use ((:instance inv-da-lha (n (+ N 2)))
			(:instance |+1+N=N+1| (n (+ n 2)))
			))))

(defthm group-operation-zero-da-n+3
  (implies (and (inv-da (+ n 3) a)
		(integerp n))
	   (equal (group-operation-da (+ n 3) (zero-da (+ n 3)) a)
		  a)))


(defthm lha-lha-n+2
  (implies (and (inv-da (+ n 1) a)
		(integerp n))
	   (equal (LHA (+ N 2) (LHA (+ n 1) a))
		  (ZERO-DA (+ N 3))))
  :hints (("Goal" :in-theory (disable LhA-1+N ZERO-da+1+N )
	   :use ((:instance lha-lha-n (n (+ n 1)))
		 (:instance |+1+N=N+1|)
		 (:instance |+1+N=N+1| (n (+ n 1)))
		 (:instance |+1+N=N+1| (n (+ n 2)))))))


(defthm inv-ha+1+n-1
  (implies (integerp n)
	   (equal (INV-HA (+ 1 N -1) a)
		  (inv-ha n a)))
  :hints (("Goal" :use (:instance |+1+N-1=N|))))


(defthm inv-ha+1+n
  (implies (integerp n)
	   (equal (inv-ha (+ 1 n) a)
		  (inv-ha (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))

(defthm d-ha+1+n
  (implies (integerp n)
	   (equal (d-ha (+ 1 n) a)
		  (d-ha (+ n 1) a)))
  :hints (("Goal" :use (:instance |+1+N=N+1|))))


(defthm inv-d-ha+n+1-help
  (implies (and (inv-ha n a)
		(integerp n))
	   (inv-ha (+ n -1) (D-ha n a)))
  :rule-classes nil)

(defthm inv-d-ha+n+1
  (implies (and (inv-ha (+ n 1) a)
		(integerp n))
	   (inv-ha n (D-ha (+ N 1) a)))
  :hints (("Goal" :use ((:instance inv-d-ha+n+1-help (n (+ N 1)))
			(:instance |+N+0=N|)))))


(defthm inverse-hb-1+n
  (implies (integerp n)
	   (equal (inverse-hb (+ -1 n) a)
		  (inverse-hb (+ n -1) a)))
  :hints (("Goal" :use (:instance |-1+N=N-1|))))

(defthm group-operation-ha-1+n-1
  (implies (integerp n)
	   (equal (GROUP-OPERATION-ha (+ 1 n -1) a b)
		  (GROUP-OPERATION-ha n a b)))
  :hints (("Goal" :use ((:instance |+1+N-1=N|)))))


(defthm external-ha-1+n-1
  (implies (integerp n)
	   (equal (external-ha (+ 1 n -1) a b)
		  (external-ha n a b)))
  :hints (("Goal" :use ((:instance |+1+N-1=N|)))))


(defthm zero-ha-1+n-1
  (implies (integerp n)
	   (equal (zero-ha (+ 1 n -1))
		  (zero-ha n)))
  :hints (("Goal" :use ((:instance |+1+N-1=N|)))))

(defthm inverse-ha-1+n-1
  (implies (integerp n)
	   (equal (inverse-ha (+ 1 n -1) a)
		  (inverse-ha n a)))
  :hints (("Goal" :use ((:instance |+1+N-1=N|)))))


(defthm d-ha-1+n-1
  (implies (integerp n)
	   (equal (d-ha (+ 1 n -1) a)
		  (d-ha n a)))
  :hints (("Goal" :use ((:instance |+1+N-1=N|)))))

(defthm d-ha-1+n+1
  (implies (integerp n)
	   (equal (d-ha (+ -1 n 1) a)
		  (d-ha n a)))
  :hints (("Goal" :use ((:instance |-1+N+1=N|)))))

(defthm zero-ha-1+n-1+1
  (implies (integerp n)
	   (equal (zero-ha (+ 1 -1 -1 n))
		  (zero-ha (+ N -1))))
  :hints (("Goal" :use ((:instance |+1-1-1+N=N-1|)))))


(defthm group-operation-ha+n-1
  (implies (integerp n)
	   (equal (GROUP-OPERATION-ha (+ -1 n) a b)
		  (GROUP-OPERATION-ha (+ N -1) a b)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)))))


(defthm rfa+n-1
  (implies (integerp n)
	   (equal (rfa (+ -1 n) a)
		  (rfa (+ N -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)))))


(defthm rgb+n-1
  (implies (integerp n)
	   (equal (rgb (+ -1 n) a)
		  (rgb (+ N -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1|)))))



(defthm group-operation-zero-ha-n-1
  (implies (and (inv-ha (+ n -1) a)
		(integerp n))
	   (equal (group-operation-ha (+ n -1) (zero-ha (+ n -1)) a)
		  a)))



(defthm zero-d-ha-d-ha-1
  (implies (and (inv-ha n a)
		(integerp n))
	   (equal (D-ha (+ -1 n) (D-ha n a))
		  (zero-ha (+ -1 (+ -1 n)))))
  :hints (("Goal" :in-theory (disable ASSOCIATIVITY-OF-+)))
  :rule-classes nil)


(DEFTHM |-1-1+N+1=N-1|
  (IMPLIES (INTEGERP N)
	   (EQUAL (+ -1 -1 (+ N 1)) (+ N -1)))
  :RULE-CLASSES NIL)

(defthm zero-ha+1+n-1-1
  (implies (integerp n)
	   (equal (zero-ha (+ -1 -1 (+ N 1)))
		  (zero-ha (+ N -1))))
  :hints (("Goal" :use ((:instance |-1-1+N+1=N-1|)))))


(defthm zero-d-ha-d-ha
  (implies (and (inv-ha (+ n 1) a)
		(integerp n))
	   (equal (D-ha N (D-ha (+ N 1) a))
		  (zero-ha (+ N -1))))
  :hints (("Goal" 
	   :use ((:instance zero-d-ha-d-ha-1 (n (+ N 1)))
		 )))
  )


(defthm d-hb-1+n
  (implies (integerp n)
	   (equal (d-hb (+ -1 n) a)
		  (d-hb (+ n -1) a)))
  :hints (("Goal" :use (:instance |-1+N=N-1|))))

(defthm zero-d-hb-d-hb-1
  (implies (and (inv-hb n a)
		(integerp n))
	   (equal (D-hb (+ -1 n) (D-hb n a))
		  (zero-hb (+ -1 (+ -1 n)))))
  :hints (("Goal" :in-theory (disable D-HB-1+N ASSOCIATIVITY-OF-+)))
  :rule-classes nil)


(defthm zero-d-hb-d-hb-1-2
  (implies (and (inv-hb n a)
		(integerp n))
	   (equal (D-hb (+ n -1) (D-hb n a))
		  (zero-hb (+ n -2))))
  :hints (("Goal" :in-theory (disable D-HB-1+N )
	   :use ((:instance |-1+N=N-1|)
		 (:instance |-1+N=N-1| (n (+ n -1)))))))
  


(defthm inverse-inverse-hb+n-2
  (implies (and (inv-hb (+ n -2) a)
		(integerp n))
	   (equal (inverse-hb (+ n -2) (inverse-hb (+ n -2) a))
		  a)))


(defthm zero-d-hb
  (implies (integerp n)
	   (equal (zero-hb (+ -1 -1 N) )
		  (zero-hb (+ N -2))))
  :hints (("Goal" 
	   :use ((:instance |-1-1+N=N-2| )
		 )))
  )

(defthm group-operation-ha+n+1
  (implies (integerp n)
	   (equal (GROUP-OPERATION-ha (+ 1 n) a b)
		  (GROUP-OPERATION-ha (+ N 1) a b)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)))))


(defthm rfa+n1
  (implies (integerp n)
	   (equal (rfa (+ 1 n) a)
		  (rfa (+ N 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1| )))))


(defthm external-ha+n+1
  (implies (integerp n)
	   (equal (external-ha (+ 1 n) a b)
		  (external-ha (+ N 1) a b)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)))))

(defthm inverse-ha+n+1
  (implies (integerp n)
	   (equal (inverse-ha (+ 1 n) a)
		  (inverse-ha (+ N 1) a)))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)))))


(defthm zero-ha+n+1
  (implies (integerp n)
	   (equal (zero-ha (+ 1 n) )
		  (zero-ha (+ N 1) )))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)))))



(defthm rfa+n+0
  (implies (integerp n)
	   (equal (rfa (+ n 0) a)
		  (rfa n a)))
  :hints (("Goal" :use ((:instance |+N+0=N| )))))

(defthm group-operation-ha+n+0
  (implies (integerp n)
	   (equal (group-operation-ha (+ n 0) a b)
		  (group-operation-ha n a b)))
  :hints (("Goal" :use ((:instance |+N+0=N| )))))

(defthm j+n+0
  (implies (integerp n)
	   (equal (j (+ n 0) a)
		  (j n a)))
  :hints (("Goal" :use ((:instance |+N+0=N| )))))

(defthm lfb+n+0
  (implies (integerp n)
	   (equal (lfb (+ n 0) a)
		  (lfb n a)))
  :hints (("Goal" :use ((:instance |+N+0=N| )))))

(defthm rhb+n+0
  (implies (integerp n)
	   (equal (rhb (+ -1 n) a)
		  (rhb (+ n -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1| )))))

(defthm rfb+n+0
  (implies (integerp n)
	   (equal (rfb (+ -1 n) a)
		  (rfb (+ n -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1| )))))


(defthm rha+n+1
  (implies (integerp n)
	   (equal (rha (+ 1 n) a )
		  (rha (+ N 1) a )))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)))))



(DEFTHM INV-DA-rHA
  (IMPLIES (AND (INV-DA N A) (INTEGERP N))
	   (INV-DA (+ 1 N) (rHA N A))))

(defthm inv-da-rha+n+2
  (implies (and (inv-da (+ N 1) a)
		(integerp n))
	   (inv-da (+ n 2) (rha (+ N 1) a)))
  :hints (("Goal" :use ((:instance inv-da-rha (n (+ N 1)))
			(:instance |+1+N=N+1| (n (+ n 1)))
			))))

(defthm rga+n+1
  (implies (integerp n)
	   (equal (rga (+ 1 n) a )
		  (rga (+ N 1) a )))
  :hints (("Goal" :use ((:instance |+1+N=N+1|)))))


(defthm inverse-da-1+n+1
  (implies (integerp n)
	   (equal (inverse-da (+ -1 n 1) a)
		  (inverse-da n a)))
  :hints (("Goal" :use ((:instance |-1+N+1=N|)))))


(defthm rga-1+n+1
  (implies (integerp n)
	   (equal (rga (+ -1 n 1) a)
		  (rga n a)))
  :hints (("Goal" :use ((:instance |-1+N+1=N|)))))


(defthm rha-1+n
  (implies (integerp n)
	   (equal (rha (+ -1 n) a)
		  (rha (+ n -1) a)))
  :hints (("Goal" :use ((:instance |-1+N=N-1| )))))

(defthm rha+n+0
  (implies (integerp n)
	   (equal (rha (+ n 0) a)
		  (rha n a)))
  :hints (("Goal" :use ((:instance |+N+0=N| )))))

;***;

(in-theory (disable inv-CONE-CONE-D2-D1-CONE-SES3 group-operation-CONE-CONE-D2-D1-CONE-SES3 zero-CONE-CONE-D2-D1-CONE-SES3 external-CONE-CONE-D2-D1-CONE-SES3 inverse-CONE-CONE-D2-D1-CONE-SES3 d-CONE-CONE-D2-D1-CONE-SES3 
   inv-CONE-CONE-h2-h1-CONE-SES3 group-operation-CONE-CONE-H2-H1-CONE-SES3 zero-CONE-CONE-H2-H1-CONE-SES3 external-CONE-CONE-H2-H1-CONE-SES3 inverse-CONE-CONE-H2-H1-CONE-SES3 d-CONE-CONE-H2-H1-CONE-SES3    
   NEW-F-CONE-DJ-CC  NEW-g-CONE-Dj-CC NEW-H-CONE-Dj-CC Rf-CONES-CONE-SES3 Rg-CONES-CONE-SES3 RH-CONES-CONE-SES3
   |CONE->C-is-a-reduction|
))




;; |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|
;; |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence-CONE-SES3|
 


(defthm lema1 (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		   (INV-CONE-CONE-D2-D1-CONE-SES3 N B)
		    (INV-CONE-CONE-D2-D1-CONE-SES3 N C)
		   (INTEGERP N))
	      (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3
		      N A
		      (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3 N B C))
	       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3
		      N C
		      (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3 N A B))
		     ))
     :hints (("Goal" :use (:instance |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence-CONE-SES3|)))
)

(defthm lema1-b (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		   (INV-CONE-CONE-D2-D1-CONE-SES3 N B)
		    (INV-CONE-CONE-D2-D1-CONE-SES3 N C)
		   (INTEGERP N))
	      (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3
		      N A
		      (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3 N B C))
	       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3
		      N b
		      (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3 N A c))
		     ))
     :hints (("Goal" :use (:instance |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence-CONE-SES3|)))
)


(defthm lema2
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		(INTEGERP N))
	   (INV-C_C N (NEW-F-CONE-DJ-CC N A)))
   :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)


(defthm lema3
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		(INV-CONE-CONE-D2-D1-CONE-SES3 N B)
		(INTEGERP N))
	   (EQUAL (NEW-F-CONE-DJ-CC N
                         (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3 N A B))
		  (GROUP-OPERATION-C_C N (NEW-F-CONE-DJ-CC N A)
				       (NEW-F-CONE-DJ-CC N B)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema4
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		(INV-RING-R R)
		(INTEGERP N))
	   (EQUAL (NEW-F-CONE-DJ-CC N
                         (EXTERNAL-CONE-CONE-D2-D1-CONE-SES3 N R A))
       (EXTERNAL-C_C N R (NEW-F-CONE-DJ-CC N A)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

;;
(defthm lema5
  (implies (integerp n)
	   (EQUAL (NEW-F-CONE-DJ-CC N (ZERO-CONE-CONE-D2-D1-CONE-SES3 N))
       (ZERO-C_C N)))
  :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema6
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		
		(INTEGERP N))
	   (EQUAL (NEW-F-CONE-DJ-CC N
                         (INVERSE-CONE-CONE-D2-D1-CONE-SES3 N A))
       (INVERSE-C_C N (NEW-F-CONE-DJ-CC N A)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)


(defthm lema7
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		
		(INTEGERP N))
	   (EQUAL (D-C_C N (NEW-F-CONE-DJ-CC N A))
       (NEW-F-CONE-DJ-CC (+ -1 N)
                         (D-CONE-CONE-D2-D1-CONE-SES3 N A)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema8
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		
		(INTEGERP N))
	   (INV-CONE-CONE-D2-D1-CONE-SES3 (+ N 1)
                               (NEW-H-CONE-DJ-CC N A))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)


(defthm lema9
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		(INV-CONE-CONE-D2-D1-CONE-SES3 N B)
		(INTEGERP N))
	   (EQUAL (NEW-H-CONE-DJ-CC N
                         (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3 N A B))
       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3 (+ N 1)
                                                  (NEW-H-CONE-DJ-CC N A)
                                                  (NEW-H-CONE-DJ-CC N B)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema10
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		(INV-RING-R R)
		(INTEGERP N))
	   (EQUAL (NEW-H-CONE-DJ-CC N
                         (EXTERNAL-CONE-CONE-D2-D1-CONE-SES3 N R A))
       (EXTERNAL-CONE-CONE-D2-D1-CONE-SES3 (+ N 1)
                                           R (NEW-H-CONE-DJ-CC N A)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)
;;

(defthm lema11
  (implies (and 
		(INTEGERP N))
	   (EQUAL (NEW-H-CONE-DJ-CC N (ZERO-CONE-CONE-D2-D1-CONE-SES3 N))
       (ZERO-CONE-CONE-D2-D1-CONE-SES3 (+ N 1)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema12
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N A)
		
		(INTEGERP N))
	   (EQUAL (NEW-H-CONE-DJ-CC N
                         (INVERSE-CONE-CONE-D2-D1-CONE-SES3 N A))
       (INVERSE-CONE-CONE-D2-D1-CONE-SES3 (+ N 1)
                                          (NEW-H-CONE-DJ-CC N A)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema13
  (implies (and (INV-C_C N A)
		
		(INTEGERP N))
	   (INV-CONE-CONE-D2-D1-CONE-SES3 N (NEW-G-CONE-DJ-CC N A))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)


(defthm lema14
  (implies (and (INV-C_C N A)
		(INV-C_C N B)
		(INTEGERP N))
	   (EQUAL (NEW-G-CONE-DJ-CC N (GROUP-OPERATION-C_C N A B))
       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3 N (NEW-G-CONE-DJ-CC N A)
                                                  (NEW-G-CONE-DJ-CC N B)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema15
  (implies (and (INV-C_C N A)
		(INV-RING-R R)
		(INTEGERP N))
	   (EQUAL (NEW-G-CONE-DJ-CC N (EXTERNAL-C_C N R A))
       (EXTERNAL-CONE-CONE-D2-D1-CONE-SES3 N R (NEW-G-CONE-DJ-CC N A)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)


(defthm lema17
  (implies (and 
		(INTEGERP N))
	   (EQUAL (NEW-G-CONE-DJ-CC N (ZERO-C_C N))
       (ZERO-CONE-CONE-D2-D1-CONE-SES3 N))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema18
  (implies (and (INV-C_C N A)
		
		(INTEGERP N))
	   (EQUAL (NEW-G-CONE-DJ-CC N (INVERSE-C_C N A))
       (INVERSE-CONE-CONE-D2-D1-CONE-SES3 N (NEW-G-CONE-DJ-CC N A)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema19
  (implies (and (INV-C_C N A)
		
		(INTEGERP N))
	   (EQUAL (D-CONE-CONE-D2-D1-CONE-SES3 N (NEW-G-CONE-DJ-CC N A))
       (NEW-G-CONE-DJ-CC (+ -1 N) (D-C_C N A)))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)


(defthm lema20
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES3 N GNRT)
		
		(INTEGERP N))
	   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3
            N
            (NEW-H-CONE-DJ-CC (+ -1 N)
                              (D-CONE-CONE-D2-D1-CONE-SES3 N GNRT))
            (D-CONE-CONE-D2-D1-CONE-SES3 (+ 1 N)
                                         (NEW-H-CONE-DJ-CC N GNRT)))
       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES3
            N GNRT
            (INVERSE-CONE-CONE-D2-D1-CONE-SES3
                 N
                 (NEW-G-CONE-DJ-CC N (NEW-F-CONE-DJ-CC N GNRT)))))
	   )
     :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DJ-CC|)))
)

(defthm lema21-help (implies (and (INV-CONE-CONE-H2-H1-CONE-SES3 N A)
		   (INV-CONE-CONE-H2-H1-CONE-SES3 N b)
		    
		   (INTEGERP N))
	      (EQUAL (GROUP-OPERATION-CONE-CONE-h2-h1-CONE-SES3
		      N A b)
		      
	       (GROUP-OPERATION-CONE-CONE-h2-h1-CONE-SES3
		      N b a)
		      ))
     :hints (("Goal" :use (:instance |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence-CONE-SES3|)))
)

(defthm lema21-help2
  (IMPLIES
          (AND (INV-CONE-CONE-H2-H1-CONE-SES3 N A)
               (INV-CONE-CONE-H2-H1-CONE-SES3 N B)
               (INV-CONE-CONE-H2-H1-CONE-SES3 N C)
               (INTEGERP N))
          (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES3
                      N
                      (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES3 N A B)
                      C)
                 (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES3
                      N A
                      (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES3 N B C))))
   :hints (("Goal" :use (:instance |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence-CONE-SES3|)))
)


(defthm lema21 (implies (and (INV-CONE-CONE-H2-H1-CONE-SES3 N A)
		   (INV-CONE-CONE-H2-H1-CONE-SES3 N b)
		    (INV-CONE-CONE-H2-H1-CONE-SES3 N c)
		   (INTEGERP N))
	      (EQUAL (GROUP-OPERATION-CONE-CONE-h2-h1-CONE-SES3
		      N A
		      (GROUP-OPERATION-CONE-CONE-h2-h1-CONE-SES3 N B C))
	       (GROUP-OPERATION-CONE-CONE-h2-h1-CONE-SES3
		      N b
		      (GROUP-OPERATION-CONE-CONE-h2-h1-CONE-SES3 N A c))
		     ))
     :hints (("Goal" 
	      :use ((:instance lema21-help2)
			   (:instance lema21-help
				     (a (GROUP-OPERATION-CONE-CONE-h2-h1-CONE-SES3 N B C))
				     (b a)))))
)



(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-CONE-CONE-D2-D1-CONE-SES3 'group-operation-CONE-CONE-D2-D1-CONE-SES3 'zero-CONE-CONE-D2-D1-CONE-SES3 'external-CONE-CONE-D2-D1-CONE-SES3 'inverse-CONE-CONE-D2-D1-CONE-SES3 'd-CONE-CONE-D2-D1-CONE-SES3 
   ) 
  (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
   'inv-C_C 'group-operation-C_C 'zero-C_C 'external-C_C 'inverse-C_C 'd-C_C)
  'NEW-F-CONE-DJ-CC  'NEW-g-CONE-DJ-CC 'NEW-H-CONE-DJ-CC
  )
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
    'inv-CONE-CONE-D2-D1-CONE-SES3 'group-operation-CONE-CONE-D2-D1-CONE-SES3 'zero-CONE-CONE-D2-D1-CONE-SES3 'external-CONE-CONE-D2-D1-CONE-SES3 'inverse-CONE-CONE-D2-D1-CONE-SES3 'd-CONE-CONE-D2-D1-CONE-SES3 
   )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
   'inv-CONE-CONE-h2-h1-CONE-SES3 'group-operation-CONE-CONE-H2-H1-CONE-SES3 'zero-CONE-CONE-H2-H1-CONE-SES3 'external-CONE-CONE-H2-H1-CONE-SES3 'inverse-CONE-CONE-H2-H1-CONE-SES3 'd-CONE-CONE-H2-H1-CONE-SES3)
  'Rf-CONES-CONE-SES3 'Rg-CONES-CONE-SES3 'RH-CONES-CONE-SES3
  ))
 'homotopy-equivalence-C
   )













